Some renaming to avoid confusion between saturations and o_saturations.

[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 6a9d7794db701429f657746dc1b41dc4922aad58..e90ec7fe401942dc219b7d98be8669760cd9fabd 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
@@ -45,7 +45,7 @@ record concrete_space : Type2 ≝
  { bp:> BP;
    (*distr : is_distributive (form bp);*)
    downarrow: unary_morphism1 (form bp) (form bp);
-   downarrow_is_sat: is_saturation ? downarrow;
+   downarrow_is_sat: is_o_saturation ? downarrow;
    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);