aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index df1b82a98c..fbb3b55412 100644
--- a/CHANGES
+++ b/CHANGES
@@ -436,6 +436,9 @@ Extraction
possible if several branches are identical. For instance, functions
corresponding to decidability of equalities are now linear instead of
quadratic.
+- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
+ conflits with existing code, for instance when extracting module List
+ to Ocaml.
CoqIDE