From 5592007ae13ad8a6d4658dd8702c5627e0423d51 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 19 Sep 2001 15:21:50 +0000
Subject: Changement de syntaxe Extract Constant / Extract Inlined Constant

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

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index de52e936d3..3e630e20d7 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -120,6 +120,9 @@ The syntax is the following:
 \item{\tt Extract Constant \qualid\ => \str.} ~\par
   Give an ML extraction for the given constant.
   The \str\ may be an identifier or a quoted string.
+\item{\tt Extract Inlined Constant \qualid\ => \str.} ~\par
+  Same as the previous one, except that the given ML terms will
+  be inlined everywhere instead of being declared via a let.
 \item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots \str\ ].} ~\par
   Give an ML extraction for the given inductive type. You must specify
   extractions for the type itself (first \str) and all its
@@ -128,10 +131,10 @@ The syntax is the following:
 \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 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
-- 
cgit v1.2.3