3 files changed, 21 insertions, 13 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1459141d1e..c69c7e4001 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -93,7 +93,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/flags.ml b/lib/flags.ml
index d29064c97f..65873e5214 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,17 +112,22 @@ 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 | V8_5 | Current) -> false
-| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false
-| V8_4, (V8_4 | V8_5 | Current) -> false
-| V8_5, (V8_5 | Current) -> false
-| Current, Current -> false
-| V8_3, V8_2 -> true
-| V8_4, (V8_2 | V8_3) -> true
-| V8_5, (V8_2 | V8_3 | V8_4) -> true
-| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 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
@@ -226,7 +231,7 @@ let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
 let profile_ltac = ref false
-let profile_ltac_cutoff = ref 0.0
+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 839c252cbb..9dc0c9c048 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 | 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