X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_eq.ma;h=6773470b0bf1cce469498fb0dacb4a6a15bcefda;hb=25871137d6571c7634c967c3b2fc87eab75b9704;hp=7634cbde1171f65fa92d126eea1c8a872fc2f971;hpb=267291d2a2a35b1a9cffa78f7e435a7946df0092;p=helm.git

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 7634cbde1..6773470b0 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: dev'essere aggiornato *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
 
 include "class_defs.ma".
@@ -27,4 +29,4 @@ qed.
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
 intros; elim H; clear H.; auto.
 qed.
-*)
\ No newline at end of file
+*)