mod change (-x)

[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
old mode 100755 (executable)
new mode 100644 (file)
index 213c68b..26d5913
--- 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))).