diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/DebugPrint.ml | 2 | ||||
| -rw-r--r-- | common/Memory.v | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index d94b31d8..83a485b0 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -133,7 +133,7 @@ let print_instructions insts code = debug "[ "; List.iter ( fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code)) - ) insts; debug "]" + ) insts; debug " ]" end let print_arrayp arr = begin diff --git a/common/Memory.v b/common/Memory.v index bf8ca083..ff17efb0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -41,8 +41,6 @@ Require Export Memdata. Require Export Memtype. Require Import Lia. -Definition default_notrap_load_value (chunk : memory_chunk) := Vundef. - (* To avoid useless definitions of inductors in extracted code. *) Local Unset Elimination Schemes. |