diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:34 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:34 +0100 |
| commit | 6af0969228e57c611e5a0876efe613055de342cd (patch) | |
| tree | cfeb33115bb53bc41c588cf75dc70ef515eceff9 /doc | |
| parent | 3690e568a36f8b418ec9c253a3188403f53021ba (diff) | |
| parent | 6734614d8ace6860e3deb1861611ba4b012cfae1 (diff) | |
Merge PR #6380: Add tactics to reset and display the Ltac profile
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 15 |
1 files changed, 15 insertions, 0 deletions
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. |