diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 46 |
1 files changed, 4 insertions, 42 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index c4afb83186..33d281798f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -21,44 +21,20 @@ val record_aux_file : bool ref val test_mode : bool ref (** Async-related flags *) -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 -type tac_error_filter = [ `None | `Only of string list | `All ] -val async_proofs_tac_error_resilience : tac_error_filter ref -val async_proofs_cmd_error_resilience : bool ref -val async_proofs_delegation_threshold : float ref +val async_proofs_is_worker : unit -> bool +(** Debug flags *) val debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref -(** Enable STM debugging *) -val stm_debug : bool ref - val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref -(* -time option: every command will be wrapped with `Time` *) -val time : bool ref - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref @@ -98,10 +74,6 @@ val is_program_mode : unit -> bool 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 - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool @@ -143,27 +115,17 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** Native code compilation for conversion and normalization *) -val native_compiler : bool ref +(** When producing vo objects, also compile the native-code version *) +val output_native_objects : 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. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref |