Changeset 1352 for src/Clight/TypeComparison.ma
- Timestamp:
- Oct 11, 2011, 12:45:16 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/TypeComparison.ma
r1350 r1352 87 87 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] 88 88 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ] 89 ]. try destruct // (*Wilmer:XXXX*) cases daemon qed.89 ]. (*Wilmer:XXXX try destruct //*) cases daemon qed. 90 90 91 91 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
Note: See TracChangeset
for help on using the changeset viewer.