diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 78 |
1 files changed, 62 insertions, 16 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index ede4629c..756d3b85 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,24 +9,51 @@ (** Global options of the system. *) val boot : bool ref +val load_init : bool ref val batch_mode : bool ref +type compilation_mode = BuildVo | BuildVio | Vio2Vo +val compilation_mode : compilation_mode ref + +type async_proofs = APoff | APonLazy | APon +val async_proofs_mode : async_proofs ref +type cache = Force +val async_proofs_cache : cache option ref +val async_proofs_n_workers : int ref +val async_proofs_n_tacworkers : int ref +val async_proofs_private_flags : string option ref +val async_proofs_is_worker : unit -> bool +val async_proofs_is_master : unit -> bool +val async_proofs_full : bool ref +val async_proofs_never_reopen_branch : bool ref +val async_proofs_flags_for_workers : string list ref +val async_proofs_worker_id : string ref +type priority = Low | High +val async_proofs_worker_priority : priority ref +val string_of_priority : priority -> string +val priority_of_string : string -> priority val debug : bool ref +val in_debugger : bool ref +val in_toplevel : bool ref + +val profile : bool val print_emacs : bool ref +val coqtop_ui : bool ref -val term_quality : bool ref +val ide_slave : bool ref +val ideslave_coqtop_flags : string option ref -val xml_export : bool ref +val time : bool ref -type load_proofs = Force | Lazy | Dont -val load_proofs : load_proofs ref +val we_are_parsing : bool ref val raw_print : bool ref val record_print : bool ref +val univ_print : bool ref -type compat_version = V8_2 | V8_3 | Current +type compat_version = V8_2 | V8_3 | V8_4 | Current val compat_version : compat_version ref val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool @@ -48,25 +75,37 @@ val if_verbose : ('a -> unit) -> 'a -> unit val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool +val program_mode : bool ref +val is_program_mode : unit -> bool + +(** Global universe polymorphism flag. *) +val make_universe_polymorphism : bool -> unit +val is_universe_polymorphism : unit -> bool + +(** Local universe polymorphism flag. *) +val make_polymorphic_flag : bool -> unit +val use_polymorphic_flag : unit -> bool + val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit -val hash_cons_proofs : bool ref - -(** Temporary activate an option (to activate option [o] on [f x y z], +(** Temporarily 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 *) +(** As [with_option], but on several flags. *) +val with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b + +(** Temporarily deactivate an option *) val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b +(** Temporarily extends the reference to a list *) +val with_extra_values : 'c list ref -> 'c list -> ('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 - (** Options for external tools *) (** Returns string format for default browser to use from Coq or CoqIDE *) @@ -74,9 +113,6 @@ val browser_cmd_fmt : string val is_standard_doc_url : string -> bool -(** 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 @@ -91,3 +127,13 @@ val camlp4bin : string ref val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int + +(* Disabling native code compilation for conversion and normalization *) +val no_native_compiler : bool ref + +(* Print the mod uid associated to a vo file by the native compiler *) +val print_mod_uid : bool ref + +val tactic_context_compat : bool ref +(** Set to [true] to trigger the compatibility bugged context matching (old + context vs. appcontext) is set. *) |