diff options
author | Jason Gross <jgross@mit.edu> | 2017-12-14 12:16:28 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-12-14 12:16:28 -0500 |
commit | 6734614d8ace6860e3deb1861611ba4b012cfae1 (patch) | |
tree | 43f82f04cb5a277ab67f09fce62cfb38069623df /doc | |
parent | 40aca595dd8e26373bfa4f6b6d4cd7d43a933210 (diff) |
Add doc+changelog entries for new LtacProf tactics
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. |