aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.txt4
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 53497ff0e5..4a0130bef0 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,10 @@
= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
=========================================
+** Notation_ops **
+
+Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+
** Logging and Pretty Printing: **
* Printing functions have been removed from `Pp.mli`, which is now a