X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2FCoRN.conf.xml;h=e904b4d4e7a3a45ea3b4413f514ca6ecff58913b;hb=562e9adf40098e11d8f0bc2711a7f665360c2231;hp=ad576e986226e7672db29a9b8a4406dad1582e96;hpb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;p=helm.git

diff --git a/components/binaries/transcript/CoRN.conf.xml b/components/binaries/transcript/CoRN.conf.xml
index ad576e986..e904b4d4e 100644
--- a/components/binaries/transcript/CoRN.conf.xml
+++ b/components/binaries/transcript/CoRN.conf.xml
@@ -8,6 +8,8 @@
     <key name="input_path">/projects/helm/exportation/CoRN</key>
     <key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
     <key name="script_type">.v</key>
-    <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt</key>
+    <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
+    <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
+    <key name="coercion">nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con</key>
   </section>
 </helm_registry>