a) update with upstream version

[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 0463cff55a25cf15797f17560fa496b5d7183495..be1c2038c1c81649100e56ed231864cbdff7b8ee 100644 (file)
--- 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) *)