X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fbasic_topologies.ma;h=b61f6191642815aa2efc4029acdff5e5ed5c0063;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=3b1e2e577f8492519e3a418a04a0903b38c7edaa;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies.ma
index 3b1e2e577..b61f61916 100644
--- 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.
 *)
+*)