- components: composed coercions mus be generated with current base uri

[helm.git] / matita / contribs / CoRN-Decl / CoRN.ma

diff --git a/matita/contribs/CoRN-Decl/CoRN.ma b/matita/contribs/CoRN-Decl/CoRN.ma
index 6a0b5b4f3691d38b32b8ef226169ab77d49e6bd5..e75ca07486cdc79fc1a13516eb1164508b09436d 100644 (file)
--- a/matita/contribs/CoRN-Decl/CoRN.ma
+++ b/matita/contribs/CoRN-Decl/CoRN.ma
@@ -619,7 +619,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 +689,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 **************************************************)