diff options
| author | Brian Campbell | 2018-09-20 15:39:23 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-20 15:39:23 +0100 |
| commit | 30e1cdf6aabe611208c50e35058ea18442aa4078 (patch) | |
| tree | 5efbd2f2d3f27bd340b719ce65794158ae44b074 /src | |
| parent | 40594e108f2b88b9463afde401e0db95aed30bf2 (diff) | |
Tidy up help text for a few options
Diffstat (limited to 'src')
| -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"); |