From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Nov 2005 16:03:38 +0000 (+0000)
Subject: fix for coercions
X-Git-Tag: V_0_7_2_3~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c784fcbfe47beaa2c399cb71b3d2b84dedc4fb76

fix for coercions
---

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
index 3e59a68d1..cbe4f567a 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
@@ -25,5 +25,6 @@ record QD: Type \def {
 
 coercion qd.
 
+(* se togli il D da acin D a non ce la fa ancora *)
 inductive iall (D:QD) (P:D \to Prop) : Prop \def
-   | iall_intro: (\forall (a:D). acin D a \to P a) \to iall D P.
+   | iall_intro: (\forall a:D. acin D a \to P a) \to iall D P.