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

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index 6f1c48404..dfff4c8a8 100644
--- 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).