From d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 18 Jul 2008 15:58:12 +0000
Subject: Rétablissement de l'option -dump-glob de coq top et de l'option
 -glob-from de coqdoc (compatibilité)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/flags.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index f2ab87b4b7..4743345de7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -82,18 +82,13 @@ let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
 
-(* Dump of globalization (to be used by coqdoc) *)
-
-let noglob = ref false
-let dump = ref false
-
-(* Flags.for the virtual machine *)
+(* Flags for the virtual machine *)
 
 let boxed_definitions = ref true
 let set_boxed_definitions b = boxed_definitions := b
 let boxed_definitions _ = !boxed_definitions 
  
-(* Flags.for external tools *)
+(* Flags for external tools *)
 
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
-- 
cgit v1.2.3