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

2 files changed, 1 insertions, 6 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index eb22d4109..cfc943413 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 5a3ccda6a..3e2988676 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}