From d06b336cc95b69aab9933b2eac5da9966ac232cb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 Oct 2001 20:25:44 +0000
Subject: MAJ V7.1

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

(limited to 'doc/Extraction.tex')

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 3e630e20d7..fa8ce6c87b 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -21,7 +21,7 @@ when possible and ``ML'' will be used to refer to any of the target
 dialects.
 
 \Rem
-The extraction mechanism has been completely rewritten in version 7.0.
+The current extraction mechanism is new from version 7.0 of {\Coq}.
 In particular, the \FW\ toplevel used as intermediate step between 
 \Coq\ and ML has been abandoned.  It is also not possible 
 any more to import ML objects in this \FW\ toplevel.
-- 
cgit v1.2.3