From 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 May 2017 15:31:16 +0200
Subject: [vernac] Remove `Qed exporting` syntax.

We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.

Next step, understand why.
---
 COMPATIBILITY | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 78dfabaa3e..b5fed7f018 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -5,6 +5,10 @@ Potential sources of incompatibilities between Coq V8.6 and V8.7
   error rather than a warning when the superfluous name is already in
   use. The easy fix is to remove the superfluous name.
 
+- Proofs ending in "Qed exporting ident, .., ident" are not supported
+  anymore. Constants generated during `abstract` are kept private to the
+  local environment.
+
 Potential sources of incompatibilities between Coq V8.5 and V8.6
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3