Changeset 3587


Ignore:
Timestamp:
Jul 20, 2015, 12:18:37 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3586 r3587  
    460460** [|#x #xs] #fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
    461461inversion(divide_continuation_on_frames ct [i])
    462 #IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS]
    463 [>IH whd in match (frame_assign_var ???); inversion(new_st)
    464 #l #p #Hns #HN]
     462[1,3:#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
     463>IH whd in match (frame_assign_var ???); inversion(new_st)
     464#l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN
     465whd normalize in HN; destruct]
     466|#lfi #llfi #IH0 #INV0 normalize nodelta #ABS cases ABS
     467|#lfi #llfi #IH0 #INV0 normalize nodelta
     468
     469
    465470cases daemon
    466471qed.
Note: See TracChangeset for help on using the changeset viewer.