mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
old mode 100755 (executable)
new mode 100644 (file)
index 56c26a9..8f5e41b
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
@@ -57,13 +57,13 @@ ndefinition memory_filter_write ≝
  return λm:mcu_type.any_status m t → word32 → aux_mod_type → byte8 → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+   (λmem.Some ? (set_mem_desc ? t s mem))
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+   (λmem.Some ? (set_mem_desc ? t s mem))
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   RS08_memory_filter_write t s addr val
  | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
@@ -75,10 +75,10 @@ ndefinition memory_filter_write_bit ≝
  return λm:mcu_type.any_status m t → word32 → oct → bool → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+    (λmem.Some ? (set_mem_desc ? t s mem))
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
-   (λmem.Some ? (set_mem_desc ? t s mem))
+    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem))