minor fixes

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index a7be5cc6c5db889bf10e791e477f149e0095182c..84f48c894282c7a1971ed4f52c63d9ab6f0a0a20 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "relations.ma".
+include "notation.ma".
 
 record basic_pair: Type1 ≝
  { concr: REL;
@@ -31,8 +32,6 @@ record relation_pair (BP1,BP2: basic_pair): Type1 ≝
    commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
  }.
 
-notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
 
 interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). 
 interpretation "formal relation" 'form_rel r = (form_rel __ r).
@@ -193,5 +192,5 @@ definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
      | apply (. (#‡e1)‡(e‡#)); assumption]]
 qed.
 
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun21 (concr _) __ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun21 ___ (relS _)).
+interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr _) __ (relS c) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ___ (relS c)).