X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs.ma;h=58725373cd7e353d9f491eec3db87d6715e4e336;hb=711b00a770c30056019a2b7204903e7fb5981940;hp=b6d6e1b3dd23cb088149fb1c509e25a0fd050fc8;hpb=b6e187ff7580c3dbec8bf467915d0ccd0dfd65a8;p=helm.git

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 b6d6e1b3d..58725373c 100644
--- 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).