X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fbasic_pairs_to_o-basic_pairs.ma;h=d787796b7aa81f8fdb3570a1b9575308045a1a5d;hb=refs%2Fheads%2Fmaster;hp=2041cec40319d333f08584ac5b15571f82ee00d2;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma
index 2041cec40..d787796b7 100644
--- a/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma
@@ -15,7 +15,7 @@
 include "formal_topology/basic_pairs.ma".
 include "formal_topology/o-basic_pairs.ma".
 include "formal_topology/relations_to_o-algebra.ma".
-
+(*
 definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
  intro b;
  constructor 1;
@@ -142,3 +142,4 @@ theorem BP_to_OBP_full: full2 ?? BP_to_OBP.
   | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
  simplify; apply (†(Hgc‡#));
 qed.   
+*)