Qed export -> Qed exporting

4 files changed, 7 insertions, 7 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index ce5708093..eaeb2cba2 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -38,7 +38,7 @@ Tactic abstract.
 - Auxiliary lemmas generated by the abstract tactic are removed from
   the global environment and inlined in the proof term when a proof
   is ended with Qed.  The behavior of 8.4 can be obtained by ending
-  proofs with "Qed export" or "Qed export ident, .., ident".
+  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
 
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 186bc9add..d388840df 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.
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index b23841cef..1e254c16b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -53,7 +53,7 @@ GEXTEND Gram
 	  VernacSolveExistential (n,c)
       | IDENT "Admitted" -> VernacEndProof Admitted
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
-      | IDENT "Qed"; IDENT "export"; l = LIST0 identref SEP "," ->
+      | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
       | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
index ee84cb94e..b3e41ab1f 100644
--- a/test-suite/success/qed_export.v
+++ b/test-suite/success/qed_export.v
@@ -3,8 +3,8 @@ Proof.
 assert True as H.
   abstract (trivial) using exported_seff.
 exact H.
-Fail Qed export a_subproof.
-Qed export exported_seff.
+Fail Qed exporting a_subproof.
+Qed exporting exported_seff.
 Check ( exported_seff : True ).
 
 Lemma b : True.