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

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

diff --git a/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
index c236dc6a8658906e306af316ac25e9b6759b6dbd..b44a42a86eaca7df52fafc86047b4f86813d0c1f 100644 (file)
--- a/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
@@ -16,7 +16,7 @@ include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
 include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
 include "formal_topology/basic_pairs.ma".
 include "formal_topology/basic_topologies.ma".
-
+(*
 definition basic_topology_of_basic_pair: basic_pair → basic_topology.
  intro bp;
  letin obt ≝ (OR (BP_to_OBP bp));
@@ -61,4 +61,5 @@ qed.
 
 lemma BBBB_faithful : failthful2 ?? VVV
 FIXME
-*)
\ No newline at end of file
+*)
+*)