diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 15 |
2 files changed, 18 insertions, 2 deletions
@@ -34,6 +34,7 @@ Tactics - The tactic "romega" is also aware now of the bodies of context variables. - Tactic "decide equality" now able to manage constructors which contain proofs. +- Added tactics reset ltac profile, show ltac profile (and variants) Vernacular Commands @@ -278,7 +279,7 @@ Changes from 8.6 to 8.6.1 - Fix bug 5550: "typeclasses eauto with" does not work with section variables. - Bug 5546, qualify datatype constructors when needed in Show Match - Bug #5535, test for Show with -emacs -- Fix bug #5486, don't reverse ids in tuples +- Fix bug #5486, don't reverse ids in tuples - Fixing #5522 (anomaly with free vars of pat) - Fix bug #5526, don't check for nonlinearity in notation if printing only - Fix bug #5255 @@ -300,7 +301,7 @@ Changes from 8.6 to 8.6.1 - show unused intro pattern warning - [future] Be eager when "chaining" already resolved future values. - Opaque side effects -- Fix #5132: coq_makefile generates incorrect install goal +- Fix #5132: coq_makefile generates incorrect install goal - Run non-tactic comands without resilient_command - Univs: fix bug #5365, generation of u+k <= v constraints - make `emit' tail recursive diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 8d82460a7..00430c07f 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1358,6 +1358,21 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop ltac profiling}. \end{quote} +\tacindex{reset ltac profile}\tacindex{show ltac profile} +The following tactics behave like the corresponding vernacular commands and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. + +\begin{quote} +{\tt reset ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile} {\qstring}. +\end{quote} + You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. |