mise a jour V7 de la commande Extraction, et des options de coqtop et coqc

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

1 files changed, 6 insertions, 6 deletions

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index cb9949d97..45f7b81e5 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -1,16 +1,16 @@
-\achapter{Execution of extracted programs in Caml and Haskell}
-\label{CamlHaskellExtraction}
-\aauthor{Benjamin Werner and Jean-Christophe Filliātre}
+\achapter{Execution of extracted programs in Objective Caml and Haskell}
+\label{Extraction}
+\aauthor{Jean-Christophe Filliātre and Pierre Letouzey}
 \index{Extraction}
 
 It is possible to use \Coq\ to build certified and relatively
 efficient programs, extracting them from the proofs of their
-specifications. The extracted objects are terms of \FW, and can be 
+specifications. The extracted objects can be 
 obtained at the \Coq\ toplevel with the command {\tt Extraction}
-(see \ref{Extraction}).
+(see \ref{ExtractionTerm}).
 
 We present here a \Coq\ module, {\tt Extraction}, which translates the
-extracted terms to ML dialects, namely Caml Light, Objective Caml and
+extracted terms to ML dialects, namely Objective Caml and
 Haskell. In the following, we will not refer to a particular dialect
 when possible and ``ML'' will be used to refer to any of the target
 dialects.