X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fexadecim.ma;h=969c22a36a5ca9a0dac93394d89a14cfc03482a6;hb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;hp=246ab983eef67519ce572b32909c6f352b8b8f0b;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/exadecim.ma b/helm/software/matita/contribs/assembly/freescale/exadecim.ma
index 246ab983e..969c22a36 100644
--- a/helm/software/matita/contribs/assembly/freescale/exadecim.ma
+++ b/helm/software/matita/contribs/assembly/freescale/exadecim.ma
@@ -1450,7 +1450,7 @@ definition nat_of_exadecim ≝
   [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
   | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
 
-coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
+coercion nat_of_exadecim.
 
 (* naturali → esadecimali *)
 let rec exadecim_of_nat n ≝