aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/prelude.sail7
1 files changed, 0 insertions, 7 deletions
diff --git a/model/prelude.sail b/model/prelude.sail
index 22d050f..5ec0b92 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -102,16 +102,9 @@ val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_en
val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-function get_config_print_instr () -> bool = false
-
val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
-function get_config_print_reg () -> bool = false
-
val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
-function get_config_print_mem () -> bool = false
-
val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
-function get_config_print_platform () -> bool = false
$ifndef FEATURE_IMPLICITS
val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)