diff options
| -rw-r--r-- | src/sail.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/sail.ml b/src/sail.ml index 4cc22c40..fc01d3b4 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -155,13 +155,13 @@ let options = Arg.align ([ "<filename> provide additional library to open in Coq output"); ( "-dcoq_undef_axioms", Arg.Set Pretty_print_coq.opt_undef_axioms, - "Generate axioms for functions that are declared but not defined"); + " generate axioms for functions that are declared but not defined"); ( "-dcoq_warn_nonex", Arg.Set Rewrites.opt_coq_warn_nonexhaustive, - "Generate warnings for non-exhaustive pattern matches in the Coq backend"); + " generate warnings for non-exhaustive pattern matches in the Coq backend"); ( "-dcoq_debug_on", Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on), - "<function> Produce debug messages for Coq output on given function"); + "<function> produce debug messages for Coq output on given function"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); @@ -220,7 +220,7 @@ let options = Arg.align ([ "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem"); ( "-ddump_flow_graphs", Arg.Set C_backend.opt_ddump_flow_graphs, - "(debug) dump flow analysis for Sail functions when compiling to C"); + " (debug) dump flow analysis for Sail functions when compiling to C"); ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), "<verbosity> (debug) verbose typechecker output: 0 is silent"); |