1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 8c9b51b86b..cb4b966b08 100644
--- a/CHANGES
+++ b/CHANGES
@@ -53,6 +53,9 @@ Focusing
 
 Vernacular Commands
 
+- Proofs ending in "Qed exporting ident, .., ident" are not supported
+  anymore. Constants generated during `abstract` are kept private to the
+  local environment.
 - The deprecated Coercion Local, Open Local Scope, Notation Local syntax
   was removed. Use Local as a prefix instead.
 - For the Extraction Language command, "OCaml" is spelled correctly.