X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_defs.ma;h=acd73c4ba686ca00ca9523bfd27130bc730df00a;hb=4bcd196e7122f3ab6775a6ae6032295912800be0;hp=ba119561956e16c043898fe57df069a1530385a6;hpb=51ba598a5d034a2cb572c58f6db4937627e914a3;p=helm.git

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index ba1195619..acd73c4ba 100644
--- 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.