From 750dcf0d40fbd5feb58c3223aa1db44e3676083a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 13 Mar 2004 10:57:14 +0000
Subject: Mise en place temporaire d'un afficheur de 'language' pour le
 traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5474 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/g_extraction.ml4 | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index a2c8bc4569..92728c7862 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -37,6 +37,21 @@ VERNAC ARGUMENT EXTEND language
 | [ "Toplevel" ] -> [ Toplevel ]
 END
 
+(* Temporary for translator *)
+if !Options.v7 then
+  let pr_language _ _ = function
+    | Ocaml -> str " Ocaml"
+    | Haskell -> str " Haskell"
+    | Scheme -> str " Scheme"
+    | Toplevel -> str " Toplevel"
+  in
+  let globwit_language = Obj.magic rawwit_language in
+  let wit_language = Obj.magic rawwit_language in
+  Pptactic.declare_extra_genarg_pprule true
+    (rawwit_language, pr_language)
+    (globwit_language, pr_language)
+    (wit_language, pr_language);
+
 (* Extraction commands *)
 
 VERNAC COMMAND EXTEND Extraction
-- 
cgit v1.2.3