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

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

diff --git a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
index 58b75fb680ececa60755fcb2e77b7105b9245254..6b07dfeb0863a9c493d9b71d90bb42361054de7d 100644 (file)
--- a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
@@ -15,7 +15,7 @@
 include "formal_topology/basic_topologies.ma".
 include "formal_topology/o-basic_topologies.ma".
 include "formal_topology/relations_to_o-algebra.ma".
-
+(*
 definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
  intros (b); constructor 1;
   [ apply (POW' b) | apply (A b) | apply (J b);
@@ -89,3 +89,4 @@ theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop.
    unfold image_coercion; cases Hg; whd; simplify; intro; simplify;
 qed.
 *)
+