ums got rid of

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 61b8f77e7582b2b0f4834537d63d1ab7909b3dc2..cbdf68fdd99c93c3620ee020e63e28a15bea8ef2 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
@@ -57,7 +57,7 @@ record concrete_space : Type ≝
    converges: ∀q1,q2.
      (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
    all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp);
-   il2: ∀I:setoid.∀p:ums I (oa_P (form bp)).
+   il2: ∀I:SET.∀p:arrows1 SET I (oa_P (form bp)).
      downarrow (oa_join ? I (d_p_i ?? downarrow p)) =
      oa_join ? I (d_p_i ?? downarrow p);
    il1: ∀q.downarrow (A ? q) = A ? q