Changeset 1566


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

Pacify changes to destruct tactic.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1545 r1566  
    123123  P e.
    124124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125 [ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126 | #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127 | #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     125[ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
     126| #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
     127| #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
     128| #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
     129| #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
    130130] qed.
    131131
  • 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'
  • src/common/PositiveMap.ma

    r1562 r1566  
    178178    cases (update A b' a r)
    179179    [ #_ normalize #E destruct
    180     | #t' #H normalize #E destruct * // #b'' #NE @H /2/
     180    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
    181181    ]
    182182  ]
     
    187187    cases (update A b' a l)
    188188    [ #_ normalize #E destruct
    189     | #t' #H normalize #E destruct * // #b'' #NE @H /2/
     189    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
    190190    ]
    191191  ]
Note: See TracChangeset for help on using the changeset viewer.