From 4b1061a2e8cb93e6c1e3a1ef016e512eda9d0f64 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 22 Mar 2015 16:56:38 +0100
Subject: Qed export -> Qed exporting

---
 COMPATIBILITY | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index ce57080932..eaeb2cba24 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
 ----------------------------------------------------------------
-- 
cgit v1.2.3