- untranslated sections of "formal_topology" commented to make it compile

[helm.git] / matita / matita / lib / formal_topology / concrete_spaces.ma

diff --git a/matita/matita/lib/formal_topology/concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces.ma
index f9f715dc68465eb10acbc13325bb7b67fefd9fcb..d7006cafb056f570ab037861435261f8eb962bef 100644 (file)
--- 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
+*)
+*)