Extraction TestCompile documented + mentionned in CHANGES

 Also includes a minor fix of the Extraction doc (a Require was missing).

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 91abaa10b1..4d19548eb3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,8 @@ Standard Library
 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.
 
 Dependencies