1 files changed, 79 insertions, 21 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5fb458588..c4c0435c5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -198,8 +198,6 @@ is understood as
            {\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
            {\tt =>} {\tacexpr}\\
-& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
-           {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
 {\it test} & ::= &
@@ -311,10 +309,11 @@ A sequence is an expression of the following form:
 \begin{quote}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
 \end{quote}
-The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated
-to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is
-then applied and $v_2$ is applied to the goals generated by the
-application of $v_1$. Sequence is left-associative.
+The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be
+a tactic value. The tactic $v_1$ is applied to the current goal,
+possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to
+produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to
+all the goals produced by the prior application. Sequence is associative.
 
 \subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}}
 %\tacindex{; [ | ]}
@@ -710,6 +709,55 @@ 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{Timing a tactic that evaluates to a term\tacindex{time\_constr}\tacindex{restart\_timer}\tacindex{finish\_timing}
+\index{Tacticals!time\_constr@{\tt time\_constr}}}
+\index{Tacticals!restart\_timer@{\tt restart\_timer}}
+\index{Tacticals!finish\_timing@{\tt finish\_timing}}
+
+Tactic expressions that produce terms can be timed with the experimental tactic
+\begin{quote}
+ {\tt time\_constr} {\tacexpr}
+\end{quote}
+which evaluates {\tacexpr\tt{ ()}}
+and displays the time the tactic expression evaluated, assuming successful evaluation.
+Time is in seconds and is machine-dependent.
+
+This tactic currently does not support nesting, and will report times based on the innermost execution.
+This is due to the fact that it is implemented using the tactics
+\begin{quote}
+ {\tt restart\_timer} {\qstring}
+\end{quote}
+and
+\begin{quote}
+ {\tt finish\_timing} ({\qstring}) {\qstring}
+\end{quote}
+which (re)set and display an optionally named timer, respectively.
+The parenthesized {\qstring} argument to {\tt finish\_timing} is also
+optional, and determines the label associated with the timer for
+printing.
+
+By copying the definition of {\tt time\_constr} from the standard
+library, users can achive support for a fixed pattern of nesting by
+passing different {\qstring} parameters to {\tt restart\_timer} and
+{\tt finish\_timing} at each level of nesting.  For example:
+
+\begin{coq_example}
+Ltac time_constr1 tac :=
+  let eval_early := match goal with _ => restart_timer "(depth 1)" end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in
+  ret.
+
+Goal True.
+  let v := time_constr
+             ltac:(fun _ =>
+                     let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in
+                     let y := time_constr1 ltac:(fun _ => eval compute in x) in
+                     y) in
+  pose v.
+Abort.
+\end{coq_example}
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}}
 \index{Ltac!let rec@\texttt{let rec}}
 \index{let@\texttt{let}!in Ltac}
@@ -875,21 +923,6 @@ Goal True.
 f (3+4).
 \end{coq_example}
 
-\item \index{appcontext@\texttt{appcontext}!in pattern}
-  \optindex{Tactic Compat Context}
-For historical reasons, {\tt context} used to consider $n$-ary applications
-such as {\tt (f 1 2)} as a whole, and not as a sequence of unary
-applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail
-to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial
-application, the matched subterms would have necessarily been
-applications with exactly the same number of arguments.
-As a workaround, one could use the following variant of {\tt context}:
-\begin{quote}
-{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{quote}
-This syntax is now deprecated, as {\tt context} behaves as intended. The former
-behavior can be retrieved with the {\tt Tactic Compat Context} flag.
-
 \end{Variants}
 
 \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}
@@ -1374,10 +1407,35 @@ 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.
 
+\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}.
+
+The following tactic behaves like {\tt idtac}, and running it compacts the heap in the
+OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}).
+
+\tacindex{optimize\_heap}
+\begin{quote}
+{\tt optimize\_heap}.
+\end{quote}
+
 \endinput
 
 \subsection{Permutation on closed lists}