Documenting the tactic-in-term construction.

2 files changed, 26 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index a4ab671ad..b517f2d2d 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1900,6 +1900,31 @@ To deactivate the display of the instances of existential variables, use
 {\tt Unset Printing Existential Instances.}
 \end{quote}
 
+\subsection{Solving existential variables using tactics}
+\index{\tt \textdollar( \ldots )\textdollar}
+
+\def\expr{\textrm{\textsl{tacexpr}}}
+
+Instead of letting the unification engine try to solve an existential variable
+by itself, one can also provide an explicit hole together with a tactic to solve
+it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a
+tactic anywhere a term is expected. The order of resolution is not specified and
+is implementation-dependent. The inner tactic may use any variable defined in
+its scope, including repeated alternations between variables introduced by term
+binding as well as those introduced by tactic binding. The expression {\expr}
+can be any tactic expression as described at section~\ref{TacticLanguage}.
+
+\begin{coq_example*}
+Definition foo (x : A) : A := $( exact x )$.
+\end{coq_example*}
+
+This construction is useful when one wants to define complicated terms using
+highly automated tactics without resorting to writing the proof-term by means of
+the interactive proof engine.
+
+This mechanism is comparable to the {\tt Declare Implicit Tactic} command
+defined at~\ref{DeclareImplicit}, except that the used tactic is local to each
+hole instead of being declared globally.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 399ea8f99..e318446a4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3813,7 +3813,7 @@ e.g. \texttt{Require Import A.}).
 
 \end{Variants}
 
-\subsubsection{\tt Declare Implicit Tactic {\tac}}
+\subsubsection{\tt Declare Implicit Tactic {\tac}}\label{DeclareImplicit}
 \comindex{Declare Implicit Tactic}
 
 This command declares a tactic to be used to solve implicit arguments