X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fr-o-basic_pairs.ma;h=e598f36cb83d86c97c83b4835995e095ebfa0ee3;hb=2e97c767bc072f5ba238725ff1f738fc91a0135a;hp=76d077cfa03cc8e2b7d5cd1fe564c5a5d5f7b0ec;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

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 76d077cfa..e598f36cb 100644
--- 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".
@@ -93,7 +93,7 @@ lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C).
   | intros; apply (#‡e); ]
 qed.
 
-notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+notation < "F x" left associative with precedence 65 for @{'map_arrows $F $x}.
 interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
 definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp[1].
@@ -252,4 +252,5 @@ STOP;
 
 *)
 
-*)
\ No newline at end of file
+*)
+*)