X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fword16.ma;h=d5bdd68bf06aed722d91093953f1a36ce053468b;hb=b7aefa8f362d07bf9042f6879252345e69da07c8;hp=c47ff7d5136da098b57822ebb495df675b88ce4f;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma
index c47ff7d51..d5bdd68bf 100644
--- a/helm/software/matita/contribs/assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/assembly/freescale/word16.ma
@@ -150,7 +150,7 @@ definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
 (* word → naturali *)
 definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
 
-coercion cic:/matita/freescale/word16/nat_of_word16.con.
+coercion nat_of_word16.
 
 (* naturali → word *)
 definition word16_of_nat ≝