From ba88c14957640e07e7605841ef122b89f2f93bda Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 9 Oct 2018 13:49:00 -0400
Subject: Add minimal CHANGES entry about compat notations

---
 CHANGES.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 302e952cf6..865e1eeb95 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -42,6 +42,14 @@ Notations
   `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is
   deprecated.
 
+- Deprecated compatibility notations will actually be removed in the
+  next version of Coq.  Uses of these notations are generally easy to
+  fix thanks to the hint contained in the deprecation warnings. For
+  projects that require more than a handful of such fixes, there is [a
+  script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py)
+  that will do it automatically, using the output of coqc. The script
+  contains documentation on its usage in a comment at the top.
+
 Tactics
 
 - Added toplevel goal selector `!` which expects a single focused goal.
-- 
cgit v1.2.3