Extraction Blacklist : a new command for avoiding conflicts with existing files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7

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