Ignore:
Timestamp:
Nov 16, 2011, 4:38:41 PM (8 years ago)
Author:
sacerdot
Message:

All files ported to new dependent inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1244 r1510  
    6363initial_state p s → initial_state p s' → s = s'.
    6464#p #s #s' #H1 #H2
    65 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15
    66 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25
     65inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16
     66inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26
    6767>e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
    6868[ 2: destruct (e1) skip (e11); @refl ]
     
    8484#p #s cases p; #globs #fns #main #H
    8585inversion H;
    86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5
     86#b #f #ge #m #e1 #e2 #e3 #e4 #e5 #e6
    8787whd in ⊢ (??%?);
    8888>e2
     
    446446    //
    447447| #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
    448     inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 <e1 in H1 H2
     448    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2
    449449    #H1 #H2
    450450    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    451     whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     451    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?);
    452452    @refl
    453453| #v #f #env #k #m @refl
Note: See TracChangeset for help on using the changeset viewer.