]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/assembly/freescale/word16.ma
a) update with upstream version
[helm.git] / helm / software / matita / contribs / assembly / freescale / word16.ma
index c47ff7d5136da098b57822ebb495df675b88ce4f..d5bdd68bf06aed722d91093953f1a36ce053468b 100644 (file)
@@ -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 ≝