diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 25 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
3 files changed, 27 insertions, 1 deletions
@@ -20,6 +20,7 @@ Specification Language now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)" (possible source of incompatibilities) - Slight changes in unification error messages. +- Added a syntax $(...)$ allowing to put tactics in terms. Tactics 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 |