X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmemory%2Fmemory_struct.ma;h=26d5913ea1154ac6ee839b66718b8d174437c507;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=213c68b0a84b59dfd1402af03f887fb48274259f;hpb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;p=helm.git

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 213c68b0a..26d5913ea 100755
--- 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))).