nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / subsets.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 4152f48529a54ea91d8ef461b6dcfd8b45144169..3c855236be7cbb1c1a6473b995e8cf16828c9bd5 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -41,7 +41,7 @@ qed.
 interpretation "powerset" 'powerset A = (powerset_setoid1 A).
 
 interpretation "subset construction" 'subset \eta.x =
- (mk_powerset_carrier _ (mk_unary_morphism1 _ CPROP x _)).
+ (mk_powerset_carrier ? (mk_unary_morphism1 ? CPROP x ?)).
 
 definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
  intros;
@@ -56,7 +56,7 @@ definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
      | apply s1; assumption]]
 qed.
 
-interpretation "mem" 'mem a S = (fun21 ___ (mem _) a S).
+interpretation "mem" 'mem a S = (fun21 ??? (mem ?) a S).
 
 definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
  intros;
@@ -71,7 +71,7 @@ definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
       apply (transitive_subseteq_operator ???? s s4) ]]
 qed.
 
-interpretation "subseteq" 'subseteq U V = (fun21 ___ (subseteq _) U V).
+interpretation "subseteq" 'subseteq U V = (fun21 ??? (subseteq ?) U V).
 
 
 
@@ -96,7 +96,7 @@ definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
      | apply (. #‡e1); assumption]]
 qed.
 
-interpretation "overlaps" 'overlaps U V = (fun21 ___ (overlaps _) U V).
+interpretation "overlaps" 'overlaps U V = (fun21 ??? (overlaps ?) U V).
 
 definition intersects:
  ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
@@ -110,7 +110,7 @@ definition intersects:
     | apply (. (#‡e)‡(#‡e1)); assumption]]
 qed.
 
-interpretation "intersects" 'intersects U V = (fun21 ___ (intersects _) U V).
+interpretation "intersects" 'intersects U V = (fun21 ??? (intersects ?) U V).
 
 definition union:
  ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
@@ -124,7 +124,7 @@ definition union:
     | apply (. (#‡e)‡(#‡e1)); assumption]]
 qed.
 
-interpretation "union" 'union U V = (fun21 ___ (union _) U V).
+interpretation "union" 'union U V = (fun21 ??? (union ?) U V).
 
 (* qua non riesco a mettere set *)
 definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
@@ -139,7 +139,7 @@ definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
      [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (fun11 __ (singleton _) a).
+interpretation "singleton" 'singl a = (fun11 ?? (singleton ?) a).
 
 definition big_intersects:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).