X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Ftranslation.ma;h=b3d82bd557063443297182d3eb8c6694d1352d78;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=0463cff55a25cf15797f17560fa496b5d7183495;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/translation.ma b/helm/software/matita/contribs/assembly/freescale/translation.ma
index 0463cff55..b3d82bd55 100644
--- a/helm/software/matita/contribs/assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/assembly/freescale/translation.ma
@@ -73,7 +73,9 @@ definition full_info_of_word16 ≝
 inductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-coercion cic:/matita/freescale/translation/t_byte8.ind#xpointer(1/1/1).
+definition c_TByte ≝ TByte.
+
+coercion c_TByte.
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 inductive MA_check : instr_mode → Type ≝
@@ -117,7 +119,9 @@ inductive MA_check : instr_mode → Type ≝
 inductive instruction : Type ≝ 
 instr: ∀i:instr_mode.opcode → MA_check i → instruction.
 
-coercion cic:/matita/freescale/translation/instruction.ind#xpointer(1/1/1).
+definition c_instr ≝ instr.
+
+coercion c_instr.
 
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)