X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-concrete_spaces.ma;h=76a1f4248ce3dad030133e2651931f55e4f23d3e;hb=8272528f48b942a80024aeb9b625d99cfe3f0f44;hp=90086b4d2f0e8646b973ef60925f8ccaee6db19b;hpb=13114a0147a28f8c7359c9c19ee254716eb5f55a;p=helm.git

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 90086b4d2..76a1f4248 100644
--- 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;