diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 186bc9add3..d388840df5 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1009,7 +1009,7 @@ 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}\comindex{Qed export} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting} \index{Tacticals!abstract@{\tt abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as @@ -1017,9 +1017,9 @@ From the outside ``\texttt{abstract \tacexpr}'' is the same as {\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 +unless the proof is ended with ``\texttt{Qed exporting}''. In such case the lemma is preserved. The syntax -``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$'' +``\texttt{Qed exporting }\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. |