Changeset 1352 for src/Clight/TypeComparison.ma

Timestamp:

Oct 11, 2011, 12:45:16 PM (9 years ago)

Author:

sacerdot

Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File:

• src/Clight/TypeComparison.ma (modified) (1 diff)

src/Clight/TypeComparison.ma

@@ -87 +87 @@
         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
-]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
+]. (*Wilmer:XXXX try destruct //*) cases daemon qed.
 
 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝