X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Ftend.ma;h=a5bf7501acf7047c91527b552f1cac1c6d82922d;hb=3deaedbac3407f8b4602b885a6405d4e0cc3e955;hp=d2decf0dc2cc7d7eac2c758d48e86d955a2000d4;hpb=9483f7e6c85ec11f88bdb219b2cebad2039b1a74;p=helm.git

diff --git a/helm/software/matita/dama/tend.ma b/helm/software/matita/dama/tend.ma
index d2decf0dc..a5bf7501a 100644
--- a/helm/software/matita/dama/tend.ma
+++ b/helm/software/matita/dama/tend.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "sequence.ma".
-include "metric_lattice.ma". (* we should probably use something weaker *)
+include "metric_space.ma".
 include "nat/orders.ma".
 
 definition tends0 ≝ 
   λO:pogroup.λs:sequence O.∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
 
 definition d2s ≝ 
-  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
+  λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k.
 
 notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
 interpretation "tends to" 'tends s x =