Fix after merge, the revert of Bind Scope applies to trunk only.

1 files changed, 4 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 161906fd72..3f7cc7c98e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,10 @@ Program
 - The "Shrink Obligations" flag now applies to all obligations, not only those
   solved by the automatic tactic.
 
+Notations
+
+- "Bind Scope" can once again bind "Funclass" and "Sortclass".
+
 Changes from V8.5beta3 to V8.5
 ==============================
 
@@ -103,9 +107,6 @@ solved by the automatic tactic.
 - Documented the Hint Cut command that allows control of the
   proof-search during typeclass resolution (see reference manual).
 
-Notations
-- "Bind Scope" can once again bind "Funclass" and "Sortclass".
-
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential