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.ml8
1 files changed, 1 insertions, 7 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 4856c20a..34c1a255 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -51,9 +51,6 @@
open PPrint
open Pretty_print_common
-let opt_lem_sequential = ref false
-let opt_lem_mwords = ref false
-
type out_type =
| Lem_ast_out
| Lem_out of string list
@@ -246,10 +243,7 @@ let output_lem filename libs defs =
let generated_line = generated_line filename in
(* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *)
let types_module = (filename ^ "_types") in
- let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in
- (* if !Pretty_print_lem.opt_sequential
- then ["State_monad"; "State"]
- else ["Prompt_monad"; "Prompt"] in *)
+ let monad_modules = ["Prompt_monad"; "Prompt"] in
let operators_module =
if !Pretty_print_lem.opt_mwords
then "Sail_operators_mwords"