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/TypeComparison.ma

    r1198 r1350  
    8787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    8888        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    89 ]. destruct; //; qed.
     89]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
    9090
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
Note: See TracChangeset for help on using the changeset viewer.