freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / opcodes / pseudo.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
index c881965acfe40cb51c417fab52149c33abbee73d..4c5e3afe8a45999872115b57d2f64ea156730094 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
@@ -139,7 +139,7 @@ unification hint 0 ≔ M:mcu_type ⊢ carr (im_is_comparable M) ≡ aux_im_type
 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 (* ********************************************* *)
 
-ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
+ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 nat.
 
 (* su tutta la lista quante volte compare il byte *)
 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝