diff options
| -rw-r--r-- | src/process_file.ml | 6 | ||||
| -rw-r--r-- | src/process_file.mli | 2 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
3 files changed, 4 insertions, 8 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index a1ce00ff..83cfd8a3 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,7 +52,7 @@ let opt_new_parser = ref false type out_type = | Lem_ast_out - | Lem_out of string list option + | Lem_out of string list let get_lexbuf f = let in_chan = open_in f in @@ -199,9 +199,7 @@ let output1 libpath out_arg filename defs = Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o end - | Lem_out None -> - output_lem f' [] defs - | Lem_out (Some libs) -> + | Lem_out libs -> output_lem f' libs defs let output libpath out_arg files = diff --git a/src/process_file.mli b/src/process_file.mli index 17088d36..88c9b9fb 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -73,7 +73,7 @@ val opt_auto_mono : bool ref type out_type = | Lem_ast_out - | Lem_out of string list option (* If present, the strings are files to open in the lem backend*) + | Lem_out of string list (* If present, the strings are files to open in the lem backend*) val output : string -> (* The path to the library *) diff --git a/src/sail.ml b/src/sail.ml index 93669c9d..9bb7cfcb 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -232,9 +232,7 @@ let main() = else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in - if !(opt_libs_lem) = [] - then output "" (Lem_out None) [out_name,ast_lem] - else output "" (Lem_out (Some (!opt_libs_lem))) [out_name,ast_lem] + output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] else ()); end |