nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-concrete_spaces.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index 90086b4d2f0e8646b973ef60925f8ccaee6db19b..76a1f4248ce3dad030133e2651931f55e4f23d3e 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -17,7 +17,7 @@ include "o-saturations.ma".
 
 definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
 intros; constructor 1;
- [ apply (λx.□_b (Ext⎽b x));
+ [ apply (λx.□⎽b (Ext⎽b x));
  | intros; apply  (†(†e));]
 qed.
 
@@ -40,7 +40,7 @@ record Oconcrete_space : Type2 ≝
  }.
 
 interpretation "o-concrete space downarrow" 'downarrow x = 
-  (fun11 __ (Odownarrow _) x).
+  (fun11 ?? (Odownarrow ?) x).
 
 definition Obinary_downarrow : 
   ∀C:Oconcrete_space.binary_morphism1 (Oform C) (Oform C) (Oform C).
@@ -52,7 +52,7 @@ intros; constructor 1;
   apply ((†e)‡(†e1));]
 qed.
 
-interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (Obinary_downarrow _) a b).
+interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 ? ? ? (Obinary_downarrow ?) a b).
 
 record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type2 ≝
  { Orp:> arrows2 ? CS1 CS2;