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 -
 ide/highlight.mll         | 2 +-
 3 files changed, 2 insertions(+), 7 deletions(-)

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}
 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 39da08906f..3acdd4f086 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -98,7 +98,7 @@ let multiword_command =
 | "Implicit" space+ "Arguments"
 | "Implicit" space+ ("Type"|"Types")
 | "Combined" space+ "Scheme"
-| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))|
+| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"))|
     ("Library"|"Inline"|"NoInline"|"Blacklist"))
 | "Recursive" space+ "Extraction" (space+ "Library")?
 | ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
-- 
cgit v1.2.3