diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-27 15:17:21 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-27 15:24:47 +0200 |
| commit | ce3ed09acebe048f1a361ed6440a520b166a13b8 (patch) | |
| tree | 18f394d16698b8a051dfe9a050de990515d80ede /CHANGES | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Extraction TestCompile documented + mentionned in CHANGES
Also includes a minor fix of the Extraction doc (a Require was missing).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -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 |