summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-01-09 16:07:06 +0000
committerBrian Campbell2018-01-09 16:07:06 +0000
commit9c01188e3630b03fd4142e1424250170fa7a65ff (patch)
tree8a3d0ac8accbdb1002062bc087c6d0c52a2eca9d /src/process_file.ml
parent8193c028274dccde0d4c972290cf2ca68d74a6eb (diff)
Tidy up monomorphisation interface
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 127a5aee..3755a83d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -133,9 +133,10 @@ let monomorphise_ast locs type_env ast =
let opts = {
auto = !opt_auto_mono;
debug_analysis = !opt_dmono_analysis;
- rewrites = !opt_mono_rewrites } in
- let ast = monomorphise (!Pretty_print_lem.opt_mwords) opts
- locs type_env ast in
+ rewrites = !opt_mono_rewrites;
+ rewrite_size_parameters = !Pretty_print_lem.opt_mwords
+ } 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
let ienv = Type_check.Env.no_casts Type_check.initial_env in
Type_check.check ienv ast