From fc7f18e8596a8b4e690ff726edb02a7cf319edbd Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Wed, 4 Nov 2009 10:14:34 +0000
Subject: Removed 'Toplevel' language from extraction documentation, since it
 is not currently supported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Extraction.tex | 6 +-----
 doc/refman/RefMan-tus.tex | 1 -
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index eb22d4109b..cfc9434139 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -75,15 +75,11 @@ environment.
 \comindex{Extraction Language}
 
 The ability to fix target language is the first and more important
-of the extraction options. Default is Ocaml. Besides Haskell and
-Scheme, another language called Toplevel is provided. It is a pseudo-Ocaml,
-with no renaming on global names: so names are printed as in \Coq.
-This third language is available only at the \Coq\ Toplevel.
+of the extraction options. Default is Ocaml.
 \begin{description}
 \item {\tt Extraction Language Ocaml}.
 \item {\tt Extraction Language Haskell}.
 \item {\tt Extraction Language Scheme}.
-\item {\tt Extraction Language Toplevel}.
 \end{description}
 
 \asubsection{Inlining and optimizations}
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 5a3ccda6a3..3e29886762 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -1922,7 +1922,6 @@ VERNAC ARGUMENT EXTEND language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
-| [ "Toplevel" ] -> [ Toplevel ]
 END
 \end{verbatim}
 
-- 
cgit v1.2.3