X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Ftend.ma;h=a9372d26dee5f47b81809d3f25a8919b3129b329;hb=11a6c88f3e717b019be2eae71711c70473b5467a;hp=a5bf7501acf7047c91527b552f1cac1c6d82922d;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/tend.ma b/helm/software/matita/contribs/dama/dama_duality/tend.ma
index a5bf7501a..a9372d26d 100644
--- a/helm/software/matita/contribs/dama/dama_duality/tend.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/tend.ma
@@ -23,6 +23,5 @@ definition d2s ≝
   λ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 = 
-  (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).