diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 1b7adc2517..35da17d546 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -260,6 +260,7 @@ Defined. \subsection{\tt apply \term} \tacindex{apply} \label{apply} +\label{eapply} This tactic applies to any goal. The argument {\term} is a term well-formed in the local context. The tactic {\tt apply} tries to @@ -329,14 +330,13 @@ Section~\ref{pattern} to transform the goal so that it gets the form generated by {\tt apply} {\term$_i$}, starting from the application of {\term$_1$}. -\item {\tt eapply \term}\tacindex{eapply}\label{eapply} +\item {\tt eapply \term}\tacindex{eapply} The tactic {\tt eapply} behaves like {\tt apply} but it does not fail when no instantiations are deducible for some variables in the - premises. Rather, it turns these variables into so-called - existential variables which are variables still to instantiate. An - existential variable is identified by a name of the form {\tt ?$n$} - where $n$ is a number. The instantiation is intended to be found + premises. Rather, it turns these variables into + existential variables which are variables still to instantiate (see + Section~\ref{evars}). The instantiation is intended to be found later in the proof. \item {\tt simple apply {\term}} \tacindex{simple apply} |