From 12db7503bfe014bd180761b04ddb3558adbe4ac9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 3 Apr 2001 08:04:44 +0000
Subject: 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
---
 doc/Extraction.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'doc/Extraction.tex')

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index cb9949d973..45f7b81e57 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.
-- 
cgit v1.2.3