From bdb6ddfea5a823fa3a4e0d3e626ab71271656895 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 20 Jun 2018 15:15:41 +0200
Subject: Mention the removal of Emacs modes in CHANGES.

---
 CHANGES | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 76e8f89296..689c1eff68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,7 +45,15 @@ Tools
   COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles
   $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS).
 
-- Remove the gallina utility (extracts specification from Coq vernacular files).
+- Removed the gallina utility (extracts specification from Coq vernacular files).
+  If you would like to maintain this tool externally, please contact us.
+
+- Removed the Emacs modes distributed with Coq. You are advised to
+  use Proof-General <https://proofgeneral.github.io/> (and optionally
+  Company-Coq <https://github.com/cpitclaudel/company-coq>) instead.
+  If your use case is not covered by these alternative Emacs modes,
+  please open an issue. We can help set up external maintenance as part
+  of Proof-General, or independently as part of coq-community.
 
 Vernacular Commands
 
-- 
cgit v1.2.3