From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 lib/flags.ml | 45 +++++++++++++++++++++++++++++----------------
 1 file changed, 29 insertions(+), 16 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 2c23ec98..0e2f7e5a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
 
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 let compilation_mode = ref BuildVo
+let compilation_output_name = ref None
 
 let test_mode = ref false
 
@@ -68,11 +69,15 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
 let async_proofs_is_master () =
   !async_proofs_mode = APon && !async_proofs_worker_id = "master"
+let async_proofs_delegation_threshold = ref 0.03
 
 let debug = ref false
 let in_debugger = ref false
@@ -103,31 +108,37 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
 
 let compat_version = ref Current
 
-let version_strictly_greater v = match !compat_version, v with
-| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
-| V8_3, (V8_3 | V8_4 | Current) -> false
-| V8_4, (V8_4 | Current) -> false
-| Current, Current -> false
-| V8_3, V8_2 -> true
-| V8_4, (V8_2 | V8_3) -> true
-| Current, (V8_2 | V8_3 | V8_4) -> true
-
+let version_compare v1 v2 = match v1, v2 with
+| V8_2, V8_2 -> 0
+| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1
+| V8_3, V8_2 -> 1
+| V8_3, V8_3 -> 0
+| V8_3, (V8_4 | V8_5 | Current) -> -1
+| V8_4, (V8_2 | V8_3) -> 1
+| V8_4, V8_4 -> 0
+| V8_4, (V8_5 | Current) -> -1
+| V8_5, (V8_2 | V8_3 | V8_4) -> 1
+| V8_5, V8_5 -> 0
+| V8_5, Current -> -1
+| Current, Current -> 0
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
+
+let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
+  | V8_5 -> "8.5"
   | Current -> "current"
 
 (* Translate *)
 let beautify = ref false
-let make_beautify f = beautify := f
-let do_beautify () = !beautify
 let beautify_file = ref false
 
 (* Silent / Verbose *)
@@ -164,7 +175,7 @@ let make_polymorphic_flag b =
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
-let warn = ref false
+let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
@@ -195,9 +206,9 @@ let is_standard_doc_url url =
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
 
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* Options for changing ocamlfind (used by coqmktop) *)
+let ocamlfind_spec = ref false
+let ocamlfind = ref Coq_config.camlbin
 
 (* Options for changing camlp4bin (used by coqmktop) *)
 let camlp4bin_spec = ref false
@@ -217,6 +228,8 @@ let native_compiler = ref false
 let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
+let profile_ltac = ref false
+let profile_ltac_cutoff = ref 2.0
 
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
-- 
cgit v1.2.3