aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cErrors.ml4
-rw-r--r--lib/cWarnings.ml2
-rw-r--r--lib/flags.ml34
-rw-r--r--lib/flags.mli2
4 files changed, 26 insertions, 16 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 38ed3f5ba..48a8305bc 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -92,7 +92,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with
let print_anomaly askreport e =
if askreport then
- hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+ hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+ str ".")
else
hov 0 (raw_anomaly e)
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 18b26254d..3c851d3fa 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
let current_loc = ref Loc.ghost
-let flags = ref ""
+let flags = ref "default"
let set_current_loc = (:=) current_loc
diff --git a/lib/flags.ml b/lib/flags.ml
index 40b7a29d2..08001f0e7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,20 +112,25 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
let compat_version = ref Current
-let version_strictly_greater v = match !compat_version, v with
-| _ , Current -> false
-| Current , _ -> true
-| _ , V8_6 -> false
-| V8_6 , _ -> true
-| _ , V8_5 -> false
-| V8_5 , _ -> true
-| _ , V8_4 -> false
-| V8_4 , _ -> true
-| _ , V8_3 -> false
-| V8_3 , _ -> true
-| V8_2 , V8_2 -> false
-
-
+let version_compare v1 v2 = match v1, v2 with
+| V8_2, V8_2 -> 0
+| V8_2, (V8_3 | V8_4 | V8_5 | V8_6 | Current) -> -1
+| V8_3, V8_2 -> 1
+| V8_3, V8_3 -> 0
+| V8_3, (V8_4 | V8_5 | V8_6 | Current) -> -1
+| V8_4, (V8_2 | V8_3) -> 1
+| V8_4, V8_4 -> 0
+| V8_4, (V8_5 | V8_6 | Current) -> -1
+| V8_5, (V8_2 | V8_3 | V8_4) -> 1
+| V8_5, V8_5 -> 0
+| V8_5, (V8_6 | Current) -> -1
+| V8_6, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
+| V8_6, V8_6 -> 0
+| V8_6, Current -> -1
+| Current, Current -> 0
+| Current, (V8_2 | V8_3 | V8_4 | V8_5 | V8_6) -> 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
@@ -230,6 +235,7 @@ 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
diff --git a/lib/flags.mli b/lib/flags.mli
index e498dc6b5..67c99a38d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -64,6 +64,7 @@ val univ_print : bool ref
type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
val compat_version : compat_version ref
+val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
@@ -149,6 +150,7 @@ val tactic_context_compat : bool ref
context vs. appcontext) is set. *)
val profile_ltac : bool ref
+val profile_ltac_cutoff : float ref
(** Dump the bytecode after compilation (for debugging purposes) *)
val dump_bytecode : bool ref