Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (9 years ago)
Author:
sacerdot
Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1344 r1350  
    176176            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
    177177            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    178                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     179                change in match (is_final ?????) with (is_final s2)
    179180                @IFE
    180181                [ #r' #FINAL #E whd in E:(??%??);
     
    416417            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
    417418            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    418                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     420                change in match (is_final ?????) with (is_final s2)
    419421                @IFE [ #r ] #F #EXECK
    420422                whd in EXECK:(??%??); destruct;
     
    687689    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
    688690    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
     691    change in match (is_final ?????) with (is_final s'')
    689692    @is_final_elim
    690693    [ #r #F whd in ⊢ (?%? → ?); #S
     
    879882            cases (exec_step ge s');
    880883            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    881                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     884                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    882885                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    883886                >(exec_inf_aux_unfold …)
     
    896899            cases (exec_step ge s');
    897900            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    898                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     901                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    899902                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    900903                >(exec_inf_aux_unfold …)
Note: See TracChangeset for help on using the changeset viewer.