X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2FCoRN.ma;h=7a39a0e59b2dd633eb8e12504ea40fc029f4e01c;hb=8134330933e377a344b5ee38890198dc0b653428;hp=6a0b5b4f3691d38b32b8ef226169ab77d49e6bd5;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/CoRN.ma b/helm/software/matita/contribs/CoRN-Decl/CoRN.ma
index 6a0b5b4f3..7a39a0e59 100644
--- a/helm/software/matita/contribs/CoRN-Decl/CoRN.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/CoRN.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/CoRN".
 
+include "preamble.ma".
+
 (* From algebra/Basics ****************************************************)
 
 (* NOTATION
@@ -619,7 +621,7 @@ coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *).
 Infix "{#Z}" := ap_Z (no associativity, at level 90).
 *)
 
-coercion cic:/CoRN/model/structures/Zsec/Zpos.con 0 (* compounds *).
+coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *).
 
 (* From reals/Bridges_LUB *************************************************)
 
@@ -689,7 +691,7 @@ Notation "( A , B )" := (pairT A B).
 
 (* From reals/Q_in_CReals *************************************************)
 
-coercion cic:/CoRN/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *).
+coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *).
 
 (* From reals/R_morphism **************************************************)