nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / dama / dama_didactic / bottom.ma

diff --git a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
index a759416edef4b0821b32e8374a1451db444b8a76..08c1b976136ef3fcba94ce955d389f7b89a4e893 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
@@ -30,7 +30,7 @@ notation "hvbox(a break ≡ b)"
   non associative with precedence 45
 for @{ 'equiv $a $b }.
 
-interpretation "uguaglianza parziale" 'equiv x y = (eq _ x y).
+interpretation "uguaglianza parziale" 'equiv x y = (eq ? x y).
 
 coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).