1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
index 17cadf037721658611ac9029e22894fded4b6c43..9c6e11ceac4a89658dfd9982b3e64373be187068 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
@@ -121,13 +121,13 @@ ndefinition mem_read_bit ≝
                λc:aux_chk_type MEM_FUNC.
                λaddr:word16.
                λo:oct.
-               opt_map ?? (mf_mem_read m c addr)
+               opt_map … (mf_mem_read m c addr)
                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b))) 
   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
                λc:aux_chk_type MEM_TREE.
                λaddr:word16.
                λo:oct.
-               opt_map ?? (mt_mem_read m c addr)
+               opt_map … (mt_mem_read m c addr)
                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
                λc:aux_chk_type MEM_BITS.
@@ -158,14 +158,14 @@ ndefinition mem_update_bit ≝
                λaddr:word16.
                λo:oct.
                λv:bool.
-               opt_map ?? (mf_mem_read m c addr)
+               opt_map … (mf_mem_read m c addr)
                 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
                λc:aux_chk_type MEM_TREE.
                λaddr:word16.
                λo:oct.
                λv:bool.
-               opt_map ?? (mt_mem_read m c addr)
+               opt_map … (mt_mem_read m c addr)
                 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
                λc:aux_chk_type MEM_BITS.