remarques concernant l'extraction

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

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 0af34a9639..de52e936d3 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -127,6 +127,17 @@ The syntax is the following:
   ML recursive datatype.
 \end{description}
 
+\begin{Remarks}
+\item 
+  The given ML terms are always inlined; thus, it may be
+  useful to introduce definitions in a separate ML module and then to
+  use the corresponding qualified names.
+\item
+  The extraction of a module depending on axioms from another module
+  will not fail. It is the responsability of the ``extractor'' of that
+  other module to realize the given axioms.
+\end{Remarks}
+
 \Example
 Typical examples are the following:
 \begin{coq_example}