diff options
| -rwxr-xr-x | doc/Extraction.tex | 11 |
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} |