From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:35:04 +0100
Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously
---
 COMPATIBILITY | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 3b4e8987c9..f23dbad1c5 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -33,6 +33,13 @@ Type classes.
   type information and switching to proof mode is no longer available.
   Use { } (without the vertical bars) instead.
 
+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 vehavior of 8.4 can be obtained by ending
+  proofs with "Qed export" or "Qed export ident, .., ident".
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3


From 12a5ccdf1cb69c745aa72dad923349d411682f8d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:59:11 +0100
Subject: typo

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

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index f23dbad1c5..ce57080932 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -37,7 +37,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 vehavior of 8.4 can be obtained by ending
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
   proofs with "Qed export" or "Qed export ident, .., ident".
 
 Potential sources of incompatibilities between Coq V8.3 and V8.4
-- 
cgit v1.2.3