renaming

[helm.git] / helm / software / matita / dama / tend.ma

diff --git a/helm/software/matita/dama/tend.ma b/helm/software/matita/dama/tend.ma
index d2decf0dc2cc7d7eac2c758d48e86d955a2000d4..a5bf7501acf7047c91527b552f1cac1c6d82922d 100644 (file)
--- 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 =