X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Ftend.ma;h=84d30a8fe39450aa071c6e9e92316583c5c5f132;hb=98c84d48f4511cb52c8dc03881e113bd4bd9c6ce;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..84d30a8fe 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)).