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=be1c2038c1c81649100e56ed231864cbdff7b8ee;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/translation.ma b/helm/software/matita/contribs/assembly/freescale/translation.ma
index be1c2038c..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 TByte.
+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 instr.
+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) *)