diff options
Diffstat (limited to 'lib/options.mli')
| -rw-r--r-- | lib/options.mli | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/lib/options.mli b/lib/options.mli index 731b7da4..1a5444a4 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: options.mli,v 1.25.2.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: options.mli 7740 2005-12-26 20:07:21Z herbelin $ i*) (* Global options of the system. *) @@ -17,7 +17,6 @@ val batch_mode : bool ref val debug : bool ref val print_emacs : bool ref -val emacs_str : string -> string val term_quality : bool ref @@ -27,15 +26,11 @@ 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 val translate_file : bool ref val translate_syntax : bool ref -val translate_strict_impargs : bool ref val make_silent : bool -> unit val is_silent : unit -> bool @@ -44,6 +39,8 @@ val silently : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('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 @@ -60,3 +57,14 @@ 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 head and tail of printf string format *) +(* ocaml doesn't allow not applied formats *) +val browser_cmd_fmt : string * string + |