From 17c2147fe0a73b4e0af6481afd73df5cdcf8aefd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Apr 2016 15:47:34 +0200
Subject: Fix after merge, the revert of Bind Scope applies to trunk only.

---
 CHANGES | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3