Changeset 1782


Ignore:
Timestamp:
Feb 27, 2012, 5:55:27 PM (8 years ago)
Author:
campbell
Message:

Correct bad inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/Traces.ma

    r1765 r1782  
    15341534    #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -NOT_UNDEFINED -NO_TERMINATION destruct
    15351535    inversion S
    1536     [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct ]
     1536    [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
    15371537    (* state_bound_on_steps_to_cost needs to know about the current stack frame,
    15381538       so we can use it as a witness that at least one frame exists *)
Note: See TracChangeset for help on using the changeset viewer.