nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/tend.ma b/helm/software/matita/contribs/dama/dama_duality/tend.ma
index 84d30a8fe39450aa071c6e9e92316583c5c5f132..a9372d26dee5f47b81809d3f25a8919b3129b329 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/tend.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/tend.ma
@@ -23,5 +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 = (tends0 _ (d2s _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).