diff options
Diffstat (limited to 'lib/flags.mli')
-rw-r--r-- | lib/flags.mli | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli new file mode 100644 index 00000000..1fcae990 --- /dev/null +++ b/lib/flags.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*) + +(* Global options of the system. *) + +val boot : bool ref + +val batch_mode : bool ref + +val debug : bool ref + +val print_emacs : bool ref +val print_emacs_safechar : bool ref + +val term_quality : bool ref + +val xml_export : bool ref + +val dont_load_proofs : bool ref + +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 make_silent : bool -> unit +val is_silent : unit -> bool +val is_verbose : unit -> bool +val silently : ('a -> 'b) -> 'a -> 'b +val if_silent : ('a -> unit) -> 'a -> unit +val if_verbose : ('a -> unit) -> 'a -> unit + +val make_warn : bool -> unit +val if_warn : ('a -> unit) -> 'a -> unit + +val hash_cons_proofs : bool ref + +(* Temporary activate an option ('c must be an atomic type) *) +val with_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 + +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 +val boxed_definitions : unit -> bool + +(* Options for external tools *) + +(* Returns string format for default browser to use from Coq or CoqIDE *) +val browser_cmd_fmt : string + +(* Substitute %s in the first chain by the second chain *) +val subst_command_placeholder : string -> string -> string |