Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (7 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r2353 r2391  
    383383    >(yields_eq ??? (bool_of_false ?? H2))
    384384    @refl
    385 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    386     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    387     >(yields_eq ??? (bool_of_false ?? H2))
    388     @refl
    389 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    390     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    391     >(yields_eq ??? (bool_of_true ?? H2))
    392     @refl
    393 | #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl
    394 | 13,14: #f #e #s [#cl] #k #env #m @refl
     385| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     387    >(yields_eq ??? (bool_of_false ?? H2))
     388    @refl
     389| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     391    >(yields_eq ??? (bool_of_true ?? H2))
     392    @refl
     393| #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
     394| 13,14: #f #e #s #k #env #m @refl
    395395| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    396396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     
    424424    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    425425    | #s' #k' whd in ⊢ (% → ?); *;
    426     | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
     426    | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
    427427    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
    428428    | #k' whd in ⊢ (% → ?); *;
Note: See TracChangeset for help on using the changeset viewer.