aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml15
-rw-r--r--lib/flags.mli5
2 files changed, 14 insertions, 6 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index b4f6272acf..8cce04c50f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -38,12 +38,19 @@ let record_print = ref true
(* Compatibility mode *)
-type compat_version = V8_2 | V8_3
-let compat_version = ref None
-let version_strictly_greater v =
- match !compat_version with None -> true | Some v' -> v'>v
+(* Current means no particular compatibility consideration.
+ For correct comparisons, this constructor should remain the last one. *)
+
+type compat_version = V8_2 | V8_3 | Current
+let compat_version = ref Current
+let version_strictly_greater v = !compat_version > v
let version_less_or_equal v = not (version_strictly_greater v)
+let pr_version = function
+ | V8_2 -> "8.2"
+ | V8_3 -> "8.3"
+ | Current -> "current"
+
(* Translate *)
let beautify = ref false
let make_beautify f = beautify := f
diff --git a/lib/flags.mli b/lib/flags.mli
index 77399b9e5e..0aceee0459 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -26,10 +26,11 @@ val load_proofs : load_proofs ref
val raw_print : bool ref
val record_print : bool ref
-type compat_version = V8_2 | V8_3
-val compat_version : compat_version option ref
+type compat_version = V8_2 | V8_3 | Current
+val compat_version : compat_version ref
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
+val pr_version : compat_version -> string
val beautify : bool ref
val make_beautify : bool -> unit