1 files changed, 21 insertions, 13 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index 1fcae990..c5903285 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*)
+(*i $Id: flags.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
 
 (* Global options of the system. *)
 
@@ -29,16 +29,16 @@ val raw_print : bool ref
 
 val unicode_syntax : bool ref
 
-val translate : bool ref
-val make_translate : bool -> unit
-val do_translate : unit -> bool
-val translate_file : bool ref
-val translate_syntax : bool ref
+val beautify : bool ref
+val make_beautify : bool -> unit
+val do_beautify : unit -> bool
+val beautify_file : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
@@ -47,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option ('c must be an atomic type) *)
+(* Temporary activate an option (to activate option [o] on [f x y z],
+   use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(* Temporary deactivate an option *)
+val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
 (* If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
@@ -57,12 +61,6 @@ val print_hyps_limit : unit -> int option
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
 
-(* Dump of globalization (to be used by coqdoc) *)
-
-val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-
 (* Options for the virtual machine *)
 
 val set_boxed_definitions : bool -> unit
@@ -75,3 +73,13 @@ val browser_cmd_fmt : string
  
 (* Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
+
+(* Options for specifying where coq librairies reside *)
+val coqlib_spec : bool ref
+val coqlib : string ref
+
+(* Options for specifying where OCaml binaries reside *)
+val camlbin_spec : bool ref
+val camlbin : string ref
+val camlp4bin_spec : bool ref
+val camlp4bin : string ref