many changes regarding coercions:

[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 57ec577aec9d1248c0f70e521dc62329a4dafbeb..b005216336904fc0dd6c0939bf2646386841897e 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
@@ -92,11 +92,12 @@ definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) →
  λCS1,CS2,c.rp ?? c.
 coercion rp''.
 
-definition rp''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
+
+definition rp''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
  λCS1,CS2,c.rp ?? c.
 coercion rp'''.
 
-definition rp'''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝
+definition rp'''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝
  λCS1,CS2,c.rp ?? c.
 coercion rp''''.
 
@@ -140,7 +141,7 @@ definition CSPA: category2.
     change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
     apply rule ASSOC;
   | intros; simplify;
-    change with (a ∘ id2 ? o1 = a);
+    change with (a ∘ id2 BP o1 = a);
     apply (id_neutral_right2 : ?);
   | intros; simplify;
     change with (id2 ? o2 ∘ a = a);