diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 689ac14254..1704b4d60b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1010,13 +1010,19 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export} \index{Tacticals!abstract@{\tt abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the current goal and \textit{n} is chosen so that this is a fresh name. +Such auxiliary lemma is inlined in the final proof term +unless the proof is ended with ``\texttt{Qed export}''. In such +case the lemma is preserved. The syntax +``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$'' +is also supported. In such case the system checks that the names given by the +user actually exist when the proof is ended. This tactical is useful with tactics such as \texttt{omega} or \texttt{discriminate} that generate huge proof terms. With that tool |