some minor fixes

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index b6d6e1b3dd23cb088149fb1c509e25a0fd050fc8..58725373cd7e353d9f491eec3db87d6715e4e336 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -22,8 +22,8 @@ record Obasic_pair: Type2 ≝
  }.
 
 (* FIX *)
-interpretation "basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
-interpretation "basic pair relation (non applied)" 'Vdash c = (Orel c).
+interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
+interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c).
 
 alias symbol "eq" = "setoid1 eq".
 alias symbol "compose" = "category1 composition".
@@ -38,8 +38,8 @@ record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝
  }.
  
 (* FIX *)
-interpretation "concrete relation" 'concr_rel r = (Oconcr_rel __ r). 
-interpretation "formal relation" 'form_rel r = (Oform_rel __ r). 
+interpretation "o-concrete relation" 'concr_rel r = (Oconcr_rel __ r). 
+interpretation "o-formal relation" 'form_rel r = (Oform_rel __ r). 
 
 definition Orelation_pair_equality:
  ∀o1,o2. equivalence_relation2 (Orelation_pair o1 o2).