]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / translation / IP2022_translation.ma
old mode 100755 (executable)
new mode 100644 (file)
index c3d8efc..a207c7c
@@ -43,7 +43,7 @@ ninductive IP2022_MA_check : IP2022_instr_mode → Type ≝
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)
 ndefinition IP2022_args_picker ≝
-λi:aux_im_type IP2022.λargs:IP2022_MA_check i.
+λi:IP2022_instr_mode.λargs:IP2022_MA_check i.
  match args with
   [ maINH         ⇒ nil ?
   | maIMM3 _      ⇒ nil ?