freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / memory / memory_struct.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma
index 213c68b0a84b59dfd1402af03f887fb48274259f..26d5913ea1154ac6ee839b66718b8d174437c507 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma
@@ -420,13 +420,14 @@ ndefinition bits_of_exadecim ≝
  | xE ⇒ quadruple … true  true  true  false
  | xF ⇒ quadruple … true  true  true  true
  ].
+
 ndefinition bits_of_byte8 ≝
 λb:byte8.
- mk_Array8T ? (fst4T … (bits_of_exadecim (b8h b)))
-              (snd4T … (bits_of_exadecim (b8h b)))
-              (thd4T … (bits_of_exadecim (b8h b)))
-              (fth4T … (bits_of_exadecim (b8h b)))
-              (fst4T … (bits_of_exadecim (b8l b)))
-              (snd4T … (bits_of_exadecim (b8l b)))
-              (thd4T … (bits_of_exadecim (b8l b)))
-              (fth4T … (bits_of_exadecim (b8l b))).
+ mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
+              (snd4T … (bits_of_exadecim (cnH ? b)))
+              (thd4T … (bits_of_exadecim (cnH ? b)))
+              (fth4T … (bits_of_exadecim (cnH ? b)))
+              (fst4T … (bits_of_exadecim (cnL ? b)))
+              (snd4T … (bits_of_exadecim (cnL ? b)))
+              (thd4T … (bits_of_exadecim (cnL ? b)))
+              (fth4T … (bits_of_exadecim (cnL ? b))).