1) \ldots here and there

[helm.git] / helm / software / matita / contribs / assembly / freescale / translation.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/translation.ma b/helm/software/matita/contribs/assembly/freescale/translation.ma
index be1c2038c1c81649100e56ed231864cbdff7b8ee..b3d82bd557063443297182d3eb8c6694d1352d78 100644 (file)
--- 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) *)