summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 3755a83d..9b5cd9da 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -127,6 +127,7 @@ let opt_ddump_raw_mono_ast = ref false
let opt_dmono_analysis = ref 0
let opt_auto_mono = ref false
let opt_mono_rewrites = ref false
+let opt_dall_split_errors = ref false
let monomorphise_ast locs type_env ast =
let open Monomorphise in
@@ -134,7 +135,8 @@ let monomorphise_ast locs type_env ast =
auto = !opt_auto_mono;
debug_analysis = !opt_dmono_analysis;
rewrites = !opt_mono_rewrites;
- rewrite_size_parameters = !Pretty_print_lem.opt_mwords
+ rewrite_size_parameters = !Pretty_print_lem.opt_mwords;
+ all_split_errors = !opt_dall_split_errors
} in
let ast = monomorphise opts locs type_env ast in
let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in