X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fopcode.ma;h=7b891bc8814122a41470b5e5e76002733893ac21;hb=0c302a9fda708e5019e48d14c5419a8a65190745;hp=47312085f146a5c58f104da6e63ddc4a27b17897;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/opcode.ma b/helm/software/matita/contribs/assembly/freescale/opcode.ma
index 47312085f..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 cic:/matita/freescale/opcode/any_opcode.ind#xpointer(1/1/1).
+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 cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/1).
-coercion cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/2).
+definition c_Byte ≝ Byte.
+definition c_Word ≝ Word.
+
+coercion c_Byte.
+coercion c_Word.
 
 (* opcode → naturali, per usare eqb *)
 definition magic_of_opcode ≝