From e0f9487be5ce770117a9c9c815af8c7010ff357b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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.)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'lib/options.mli')

diff --git a/lib/options.mli b/lib/options.mli
index d415f93d0..9eea81ed3 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