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

diff --git a/helm/software/matita/library/dama/russell_support.ma b/helm/software/matita/library/dama/russell_support.ma
index deb5fc950..fc75b76b4 100644
--- a/helm/software/matita/library/dama/russell_support.ma
+++ b/helm/software/matita/library/dama/russell_support.ma
@@ -18,10 +18,10 @@ 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 cic:/matita/dama/russell_support/inject.con 0 1.
+coercion inject 0 1.
 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/russell_support/eject.con.
+coercion eject.