X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_uniform.ma;h=36ba2d287503736707f4911fe6407d6fcee08d27;hb=c33fae30b4ce40198b8e1889ea1c1b58697cd567;hp=1dba15a7c00242c47bccee31ea638411660af3bf;hpb=62571dd402d272b1632b7739607d25df3552cc04;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 1dba15a7c..36ba2d287 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -202,7 +202,7 @@ intros (O s); apply mk_ordered_uniform_space;
 ]  
 qed.
 
-interpretation "Ordered uniform space segment" 'segment_set a = 
+interpretation "Ordered uniform space segment" 'segset a = 
  (segment_ordered_uniform_space _ a).
 
 (* Lemma 3.2 *)
@@ -210,7 +210,7 @@ alias symbol "pi1" = "exT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀s:‡O.
   ∀x:{[s]}.
-   ∀a:sequence (segment_ordered_uniform_space O s).
+   ∀a:sequence {[s]}.
     (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → 
       a uniform_converges x.
 intros 7; cases H1; cases H2; clear H2 H1;