Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (8 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/CexecSound.ma

    r1342 r1350  
    2828
    2929lemma bool_val_distinct: Vtrue ≠ Vfalse.
    30 % #H whd in H:(??%%); destruct; @(absurd ? e0 one_not_zero)
     30% #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)
    3131qed.
    3232
     
    5151
    5252axiom exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
    53 (*#m #v #ty #ty' #v'
     53(*Wilmer: XXXX #m #v #ty #ty' #v'
    5454cases v;
    5555[ #H whd in H:(??%?); destruct;
Note: See TracChangeset for help on using the changeset viewer.