From c784fcbfe47beaa2c399cb71b3d2b84dedc4fb76 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Nov 2005 16:03:38 +0000
Subject: [PATCH] fix for coercions

---
 helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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.
-- 
2.39.2