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=58c4f9c581718941e5df6ff10135aa0e93e44ff2;hb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;hp=3f3389337976967091957ee2e3894b84dc7a14c4;hpb=23043db144b24b8cd2072800b61137bb396f891e;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 3f3389337..58c4f9c58 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
@@ -38,8 +38,8 @@ record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝
  }.
  
 (* FIX *)
-interpretation "o-concrete relation" 'concr_rel r = (Oconcr_rel __ r). 
-interpretation "o-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).
@@ -211,7 +211,7 @@ definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (f
      | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
 qed.
 
-interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
+interpretation "fintersects" 'fintersects U V = (fun1 ??? (fintersects ?) U V).
 
 definition fintersectsS:
  ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
@@ -223,7 +223,7 @@ definition fintersectsS:
      | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
 qed.
 
-interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
+interpretation "fintersectsS" 'fintersects U V = (fun1 ??? (fintersectsS ?) U V).
 *)
 
 (*
@@ -235,22 +235,22 @@ definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
      | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
 qed.
 
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr ?) ?? (relS ?) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ??? (relS ?)).
 *)
 
 notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
-notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
-interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (Orel x)).
+notation > "□⎽term 90 b" non associative with precedence 90 for @{'box $b}.
+interpretation "Universal image ⊩⎻*" 'box x = (fun12 ? ? (or_f_minus_star ? ?) (Orel x)).
  
 notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
-notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
-interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (Orel x)).
+notation > "◊⎽term 90 b" non associative with precedence 90 for @{'diamond $b}.
+interpretation "Existential image ⊩" 'diamond x = (fun12 ? ? (or_f ? ?) (Orel x)).
 
 notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
 notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
-interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (Orel x)).
+interpretation "Universal pre-image ⊩*" 'rest x = (fun12 ? ? (or_f_star ? ?) (Orel x)).
 
 notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
 notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
-interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (Orel x)).
\ No newline at end of file
+interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).
\ No newline at end of file