summaryrefslogtreecommitdiff
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /lib/flags.mli
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli34
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