aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
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