1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 5a18da3c0..c9a8418cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,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