From e0f9487be5ce770117a9c9c815af8c7010ff357b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 26 Dec 2005 13:51:24 +0000
Subject: Suppression des parseurs et printeurs v7; suppression du traducteur
 (mécanismes de renommage des noms de constantes, de module, de ltac et de
 certaines variables liées de lemmes et de tactiques, mécanisme d'ajout
 d'arguments implicites, etc.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/options.ml  | 12 +-----------
 lib/options.mli |  3 ---
 2 files changed, 1 insertion(+), 14 deletions(-)

(limited to 'lib')

diff --git a/lib/options.ml b/lib/options.ml
index 38c6e91a18..854e302f8c 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -31,19 +31,9 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
-let v7 =
-  let transl = array_exists ((=) "-translate") Sys.argv in
-  let v7 = array_exists ((=) "-v7") Sys.argv in
-  let v8 = array_exists ((=) "-v8") Sys.argv in
-  if v8 & transl then error "Options -translate and -v8 are incompatible";
-  if v8 & v7 then error "Options -v7 and -v8 are incompatible";
-  ref (v7 or transl)
-
-let v7_only = ref false
-
 (* Translate *)
 let translate = ref false
-let make_translate f = translate := f; v7 := f; ()
+let make_translate f = translate := f
 let do_translate () = !translate
 let translate_file = ref false
 let translate_strict_impargs = ref true
diff --git a/lib/options.mli b/lib/options.mli
index d415f93d0e..9eea81ed30 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -26,9 +26,6 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
-val v7 : bool ref
-val v7_only : bool ref
-
 val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool
-- 
cgit v1.2.3