coercion command now requires an uri

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

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index ba119561956e16c043898fe57df069a1530385a6..acd73c4ba686ca00ca9523bfd27130bc730df00a 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -37,13 +37,11 @@ definition true_f \def \lambda (X:Type). \lambda (_:X). True.
 definition false_f \def \lambda (X:Type). \lambda (_:X). False.
 
 record Class: Type \def {
-   class: Type;
+   class:> Type;
    cin  : class \to Prop;
    cle1 : class \to class \to Prop
 }.
 
-coercion class. 
-
 inductive ceq (C:Class) (c1:C): C \to Prop \def
    | ceq_refl:   cin ? c1 \to ceq ? c1 c1
    | ceq_sing_r: \forall c2,c3.