Merge branch 'v8.5'

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.