coercion command now requires an uri

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / domain_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 916c91cd80f0db43d9d7db18c242529a7c46a0bd..68cbd01fa8d962b3d0a829959f45266dfbb971f0 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -24,11 +24,9 @@ include "class_defs.ma".
 *)
 
 record Domain: Type \def {
-   qd: Class
+   qd:> Class
 }.
 
-coercion qd.
-
 (* internal universal quantification *)
 inductive dall (D:Domain) (P:D \to Prop) : Prop \def
    | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P.