- transcript: bugfix

[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..41e60359f93d8d6d0b05df3c011c899fe10166b7 100644 (file)
--- a/helm/software/matita/library/dama/russell_support.ma
+++ b/helm/software/matita/library/dama/russell_support.ma
@@ -22,6 +22,6 @@ 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.