Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into JasonGross-trunk-function_scope

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 7de1015275..161906fd72 100644
--- a/CHANGES
+++ b/CHANGES
@@ -103,6 +103,9 @@ 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