Towards fullness.

[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 6476c4aebf727ac77847eac2ea097fa045484c25..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
@@ -21,8 +21,9 @@ record Obasic_pair: Type2 ≝
    Orel: arrows2 ? Oconcr Oform
  }.
 
-interpretation "basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
-interpretation "basic pair relation (non applied)" 'Vdash c = (Orel c).
+(* FIX *)
+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".
@@ -35,9 +36,10 @@ record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝
    Oform_rel: arrows2 ? (Oform BP1) (Oform BP2);
    Ocommute: ⊩ ∘ Oconcr_rel = Oform_rel ∘ ⊩
  }.
-
-interpretation "concrete relation" 'concr_rel r = (Oconcr_rel __ r). 
-interpretation "formal relation" 'form_rel r = (Oform_rel __ r). 
+ 
+(* FIX *)
+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).