From 116d97cb11b0660dec1e8932c23f7d270e97f984 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Apr 2001 12:26:35 +0000
Subject: remarques concernant l'extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8210 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Extraction.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

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}
-- 
cgit v1.2.3