update in groud_2 and models

[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 deb5fc950c628fbd01b4982a0f37a3b5db71b4f2..fc75b76b4f94a51c7243873a77702e52bbae1c12 100644 (file)
--- 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.