X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Frussell_support.ma;h=fc75b76b4f94a51c7243873a77702e52bbae1c12;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=41e60359f93d8d6d0b05df3c011c899fe10166b7;hpb=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

diff --git a/helm/software/matita/library/dama/russell_support.ma b/helm/software/matita/library/dama/russell_support.ma
index 41e60359f..fc75b76b4 100644
--- 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.