summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
authorJon French2019-03-04 14:23:55 +0000
committerJon French2019-03-04 14:23:55 +0000
commit94d40fb68bb3d36159a006b93909fc3841c92d28 (patch)
tree219c6d0ae7daf47cd6c8897895d182916e8f3815 /src/rewrites.mli
parenta7a3402ce155f13234d2d3e5198e5dbf6e0e8b82 (diff)
parent9ed89583d52ccff151fb75424975f2ac4e627a1b (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/rewrites.mli')
-rw-r--r--src/rewrites.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli
index cea227a5..811d52e8 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -59,6 +59,7 @@ val opt_dmono_analysis : int ref
val opt_auto_mono : bool ref
val opt_dall_split_errors : bool ref
val opt_dmono_continue : bool ref
+val opt_separate_execute : bool ref
(* Generate a fresh id with the given prefix *)
val fresh_id : string -> l -> id