From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 lib/flags.mli | 78 +++++++++++++++++++++++++++++++++++++++++++++++------------
 1 file changed, 62 insertions(+), 16 deletions(-)

(limited to 'lib/flags.mli')

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. *)
-- 
cgit v1.2.3