freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
index 74b7cc4e278c1575fa6d16acb7430ce3d8413b06..0fdf1b154fa4a9927ebdfe94f8e4205ffe5efa34 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
@@ -20,7 +20,8 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "freescale/aux_bases.ma".
+include "freescale/oct.ma".
+include "freescale/bitrigesim.ma".
 include "freescale/word16.ma".
 include "freescale/theory.ma".
 
@@ -124,7 +125,7 @@ ninductive instr_mode: Type ≝
 | MODE_SRT           : bitrigesim → instr_mode
 .
 
-ndefinition eq_instrmode ≝
+ndefinition eq_im ≝
 λi1,i2:instr_mode.
  match i1 with
   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
@@ -160,7 +161,7 @@ ndefinition eq_instrmode ≝
   | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]  
   | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2  ⇒ eq_oct n1 n2 | _ ⇒ false ]
   | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]  
-  | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]  
+  | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]  
   ].        
 
 (* enumerazione delle istruzioni di tutte le ALU *)