X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fconcrete_spaces.ma;h=d7006cafb056f570ab037861435261f8eb962bef;hb=d774b8f9c73e2497fb953e7feb4bc1840a464564;hp=f9f715dc68465eb10acbc13325bb7b67fefd9fcb;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces.ma
index f9f715dc6..d7006cafb 100644
--- a/matita/matita/lib/formal_topology/concrete_spaces.ma
+++ b/matita/matita/lib/formal_topology/concrete_spaces.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "formal_topology/basic_pairs.ma".
-
+(*
 (* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
    (confondendola con la coercion per gli oggetti di SET
 record concrete_space : Type[1] ≝
@@ -106,4 +106,5 @@ definition CSPA: category1.
     apply (.= id_neutral_left1 ????);
     apply refl1]
 qed.
-*)
\ No newline at end of file
+*)
+*)