Ignore:
Timestamp:
Nov 25, 2011, 6:12:47 PM (8 years ago)
Author:
campbell
Message:

Pacify changes to destruct tactic.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1521 r1566  
    294294    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    295295    ]
    296     inversion FINAL; #r''' #m' #E1 #E2 #_ #H destruct (E1 E2);
     296    inversion FINAL; #r''' #m'' #E1 #E2 #_ #H destruct (E1 E2);
    297297    @H
    298298| #tr' #s' #e' #se' #H #EXEC' #E destruct
     
    321321  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    322322#ge #tr0 #s0 #r #m #e0 #H inversion H;
    323 [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
     323[ #s #s' #tr #tr' #r' #e #m' #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    324324    destruct (E1 E2 E3 E4 E5);
    325325    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
    326326    @(star_right … STARs')
    327     [ 2: @(final_step ge tr' r m s' … EXECs')
     327    [ 2: @(final_step ge tr' r' m' s' … EXECs')
    328328    | skip
    329329    | @refl
    330330    ]
    331 | #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
     331| #s #s' #tr #tr' #r' #e #m' #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    332332    destruct;
    333333    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
Note: See TracChangeset for help on using the changeset viewer.