Adding a "time" tactical for benchmarking purposes. In case the tactic

backtracks, print time spent in each of successive calls.

1 files changed, 16 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9f65c0ef0..8e588f4e6 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -102,6 +102,7 @@ is understood as
 & | & {\tt once} {\tacexprpref}\\
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
+& | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -401,7 +402,7 @@ Branching is left-associative.
 \subsubsection[First tactic to work]{First tactic to work\tacindex{first}
 \index{Tacticals!first@{\tt first}}}
 
-Backtracking branching may be too expansive. In this case we may
+Backtracking branching may be too expensive. In this case we may
 restrict to a local, left biased, branching and consider the first
 tactic to work (i.e. which does not fail) among a panel of tactics:
 \begin{quote}
@@ -537,6 +538,20 @@ phases, we strongly advise you to not leave any {\tt timeout} in
 final scripts. Note also that this tactical isn't available on
 the native Windows port of Coq.
 
+\subsubsection{Timing a tactic\tacindex{time}
+\index{Tacticals!time@{\tt time}}}
+
+A tactic execution can be timed:
+\begin{quote}
+ {\tt time} {\qstring} {\tacexpr}
+\end{quote}
+evaluates {\tacexpr}
+and displays the time the tactic expression ran, whether it fails or
+successes. In case of several successes, the time for each successive
+runs is displayed. Time is in seconds and is machine-dependent. The
+{\qstring} argument is optional. When provided, it is used to identify
+this particular occurrence of {\tt time}.
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let}
 \index{Ltac!let rec}
 \index{let!in Ltac}