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