a) update with upstream version

[helm.git] / helm / software / matita / contribs / assembly / freescale / byte8.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index 6f1c484048ae6382d11961441ec7c286579a0b4e..dfff4c8a80e883a04467196392e85de986f19592 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma
@@ -150,7 +150,7 @@ definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 (* byte → naturali *)
 definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
 
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
 
 (* naturali → byte *)
 definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).