diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:45:17 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:47:09 +0200 |
commit | b46020a6ea52d77b49a12e6891575b3516b8d766 (patch) | |
tree | bf1fe9bc6d70ac44111f755dca30ed3c4d90b286 /lib/flags.ml | |
parent | d02c9c566c58e566a1453827038f2b49b695c0a5 (diff) | |
parent | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'lib/flags.ml')
-rw-r--r-- | lib/flags.ml | 34 |
1 files changed, 20 insertions, 14 deletions
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 |