From b2482b59cc9423c0944541cdb034d99d8c00cfad Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Dec 2008 19:07:09 +0000
Subject: 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
---
 doc/refman/Extraction.tex | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'doc/refman/Extraction.tex')

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index da9b3e7179..ba07182a6f 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -282,6 +282,30 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
 \end{coq_example}
 
+\asubsection{Avoiding conflicts with existing filenames}
+
+\comindex{Extraction Blaclist}
+
+When using {\tt Extraction Library}, the names of the extracted files
+directly depends from the names of the \Coq\ files. It may happen that
+these filenames are in conflict with already existing files, 
+either in the standard library of the target language or in other
+code that is meant to be linked with the extracted code. 
+For instance the module {\tt List} exists both in \Coq\ and in Ocaml.
+It is possible to instruct the extraction not to use particular filenames.
+
+\begin{description}
+\item{\tt Extraction Blacklist \ident \ldots \ident.} ~\par
+  Instruct the extraction to avoid using these names as filenames
+  for extracted code. 
+\item{\tt Print Extraction Blacklist.} ~\par
+  Show the current list of filenames the extraction should avoid.
+\item{\tt Reset Extraction Blacklist.} ~\par
+  Allow the extraction to use any filename.
+\end{description}
+
+For Ocaml, a typical use of these commands is
+{\tt Extraction Blacklist String List}.
 
 \asection{Differences between \Coq\ and ML type systems}
 
-- 
cgit v1.2.3

