From ce3ed09acebe048f1a361ed6440a520b166a13b8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Thu, 27 Jul 2017 15:17:21 +0200
Subject: Extraction TestCompile documented + mentionned in CHANGES

 Also includes a minor fix of the Extraction doc (a Require was missing).
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 91abaa10b..4d19548eb 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
 
-- 
cgit v1.2.3