From 8bf34547d21d417140b726fab5fdbf8625c5be95 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 6 Sep 2017 09:13:42 -0400
Subject: Mention requiring extraction/funind in CHANGES

---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index ca5172d7b7..fdf0c9d6be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -133,6 +133,13 @@ Plugins
 - The mathematical proof language (also known as declarative mode) was removed.
 - A new command Extraction TestCompile has been introduced, not meant
   for the general user but instead for Coq's test-suite.
+- The extraction plugin is no longer loaded by default. It must be
+  explicitly loaded with [Require Extraction], which is backwards
+  compatible.
+- The functional induction plugin (which provides the [Function]
+  vernacular) is no longer loaded by default. It must be explicitly
+  loaded with [Require FunInd], which is backwards compatible.
+
 
 Dependencies
 
-- 
cgit v1.2.3