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

[helm.git] / matita / matita / lib / formal_topology / r-o-basic_pairs.ma

diff --git a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma
index 0218ed8359bdf7d1cbdd5bf3b31acc3fe2303149..e598f36cb83d86c97c83b4835995e095ebfa0ee3 100644 (file)
--- a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
 include "formal_topology/apply_functor.ma".
-
+(*
 definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
 
 include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
@@ -252,4 +252,5 @@ STOP;
 
 *)
 
-*)
\ No newline at end of file
+*)
+*)