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

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

diff --git a/matita/matita/lib/formal_topology/basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies.ma
index 3b1e2e577f8492519e3a418a04a0903b38c7edaa..b61f6191642815aa2efc4029acdff5e5ed5c0063 100644 (file)
--- a/matita/matita/lib/formal_topology/basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_topologies.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/relations.ma".
 include "formal_topology/saturations.ma".
-
+(*
 record basic_topology: Type[1] ≝
  { carrbt:> REL;
    A: Ω^carrbt ⇒_1 Ω^carrbt;
@@ -209,3 +209,4 @@ theorem continuous_relation_eqS:
  apply Hcut2; assumption.
 qed.
 *)
+*)