diff options
| author | Pierre-Marie Pédrot | 2013-12-22 17:46:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-22 17:46:36 +0100 |
| commit | f9107a2ac358e161c5312984748d80c33db24ef0 (patch) | |
| tree | 1d2f9fb063d8345d8784a63cdde2753f38fe1e72 | |
| parent | db33ec1898dacbcd398c38e0a6535be931ed5fb3 (diff) | |
Adding a finer-grained -bt flag to coqtop only triggering backtraces.
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 |
2 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 68f58e6662..b75a225588 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -296,6 +296,7 @@ let parse_args arglist = |"-batch" -> set_batch_mode () |"-beautify" -> make_beautify true |"-boot" -> boot := true; no_load_rc () + |"-bt" -> Backtrace.record_backtrace true |"-color" -> Flags.make_term_color true |"-config"|"--config" -> print_config := true |"-debug" -> set_debug () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index b8e94c9ccb..8d5aebc700 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -58,13 +58,15 @@ let print_usage_channel co command = \n -init-file f set the rcfile to f\ \n -batch batch mode (exits just after arguments parsing)\ \n -boot boot mode (implies -q and -batch)\ +\n -bt print backtraces (requires configure debug flag)\ +\n -debug debug mode (implies -bt)\ \n -emacs tells Coq it is executed under Emacs\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ -\n -force-load-proofs load opaque proofs in memory initially\ +\n -force-load-proofs load opaque proofs in memory initially\ \n -lazy-load-proofs load opaque proofs in memory by necessity (default)\ \n -dont-load-proofs see opaque proofs as axioms instead of loading them\ \n -xml export XML files either to the hierarchy rooted in\ |