diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/sail.ml b/src/sail.ml index 6e5e7556..be2a6198 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -111,6 +111,9 @@ let options = Arg.align ([ ( "-latex", Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ], " pretty print the input to latex"); + ( "-latex_full_valspecs", + Arg.Clear Latex.opt_simple_val, + " print full valspecs in latex output latex"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); @@ -149,6 +152,12 @@ let options = Arg.align ([ ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); + ( "-lem_output_dir", + Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), + " set a custom directory to output generated Lem"); + ( "-isa_output_dir", + Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), + " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), "<filename> provide additional library to open in Lem output"); @@ -161,6 +170,9 @@ let options = Arg.align ([ ( "-coq", Arg.Set opt_print_coq, " output a Coq translated version of the input"); + ( "-coq_output_dir", + Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), + " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), "<filename> provide additional library to open in Coq output"); |