From f9107a2ac358e161c5312984748d80c33db24ef0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 22 Dec 2013 17:46:36 +0100 Subject: Adding a finer-grained -bt flag to coqtop only triggering backtraces. --- toplevel/coqtop.ml | 1 + toplevel/usage.ml | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) 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\ -- cgit v1.2.3