Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously

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