diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-14 01:44:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-14 01:44:53 +0200 |
| commit | 19330a458b907b5e66a967adbfe572d92194913c (patch) | |
| tree | 2d3ffa4715224082dec3c9d6f8247881ca2b1f2c /toplevel | |
| parent | 95bdd608fa7862dc28cc7f4f95578ed1a20353eb (diff) | |
| parent | d018d4148ef6cce96006bd76f83ccf46f6225e11 (diff) | |
Merge branch "LtacProf for trunk" (PR #165).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 869f6bb93..aab20650a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,6 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f855c096e..5359a288a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ +\n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ |