X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fopcode.ma;h=7b891bc8814122a41470b5e5e76002733893ac21;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=fc30ddeb414e309efc92d2a6bd2c39b1b26c6873;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/opcode.ma b/helm/software/matita/contribs/assembly/freescale/opcode.ma
index fc30ddeb4..7b891bc88 100644
--- a/helm/software/matita/contribs/assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/assembly/freescale/opcode.ma
@@ -216,15 +216,20 @@ inductive opcode: Type ≝
 inductive any_opcode (m:mcu_type) : Type ≝
  anyOP : opcode → any_opcode m.
 
-coercion anyOP.
+definition c_anyOP ≝ anyOP.
+
+coercion c_anyOP.
 
 (* raggruppamento di byte e word in un tipo unico *)
 inductive byte8_or_word16 : Type ≝
   Byte: byte8  → byte8_or_word16
 | Word: word16 → byte8_or_word16.
 
-coercion Byte.
-coercion Word.
+definition c_Byte ≝ Byte.
+definition c_Word ≝ Word.
+
+coercion c_Byte.
+coercion c_Word.
 
 (* opcode → naturali, per usare eqb *)
 definition magic_of_opcode ≝