a bit of work done while travelling to padova

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