nasty change in the lexer/parser:

[helm.git] / helm / software / matita / library / dama / russell_support.ma

diff --git a/helm/software/matita/library/dama/russell_support.ma b/helm/software/matita/library/dama/russell_support.ma
index 41e60359f93d8d6d0b05df3c011c899fe10166b7..fc75b76b4f94a51c7243873a77702e52bbae1c12 100644 (file)
--- a/helm/software/matita/library/dama/russell_support.ma
+++ b/helm/software/matita/library/dama/russell_support.ma
@@ -18,8 +18,8 @@ include "logic/cprop_connectives.ma".
 definition hide ≝ λT:Type.λx:T.x.
 
 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide = (hide _ _).
-interpretation "hide2" 'hide = (hide _ _ _).
+interpretation "hide" 'hide = (hide ? ?).
+interpretation "hide2" 'hide = (hide ? ? ?).
 
 definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
 coercion inject 0 1.