X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Ftranslation.ma;h=be1c2038c1c81649100e56ed231864cbdff7b8ee;hb=7048db496643fc440aebc6e85dd425886bcd2e56;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..be1c2038c 100644
--- a/helm/software/matita/contribs/assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/assembly/freescale/translation.ma
@@ -73,7 +73,7 @@ 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).
+coercion TByte.
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 inductive MA_check : instr_mode → Type ≝
@@ -117,7 +117,7 @@ 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).
+coercion instr.
 
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)