summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
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