X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fopcode.ma;h=fc30ddeb414e309efc92d2a6bd2c39b1b26c6873;hb=09b92a7ca6e17c21a32471816f5f4c7634e4f937;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..fc30ddeb4 100644
--- a/helm/software/matita/contribs/assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/assembly/freescale/opcode.ma
@@ -216,15 +216,15 @@ 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).
+coercion 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).
+coercion Byte.
+coercion Word.
 
 (* opcode → naturali, per usare eqb *)
 definition magic_of_opcode ≝