Add a version to be used when parsing compatibility notations mentioning old versions.

5 files changed, 28 insertions, 21 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 6a3b7a426..682e2e4df 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,32 +106,36 @@ 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 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
 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
+  | VOld, VOld -> 0
+  | VOld, _ -> -1
+  | _, VOld -> 1
+  | V8_2, V8_2 -> 0
+  | V8_2, _ -> -1
+  | _, V8_2 -> 1
+  | V8_3, V8_3 -> 0
+  | V8_3, _ -> -1
+  | _, V8_3 -> 1
+  | V8_4, V8_4 -> 0
+  | V8_4, _ -> -1
+  | _, V8_4 -> 1
+  | V8_5, V8_5 -> 0
+  | V8_5, _ -> -1
+  | _, V8_5 -> 1
+  | V8_6, V8_6 -> 0
+  | V8_6, _ -> -1
+  | _, V8_6 -> 1
+  | Current, Current -> 0
 
 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
+  | VOld -> "old"
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
diff --git a/lib/flags.mli b/lib/flags.mli
index e2cf09474..c0aca9c99 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,7 +77,7 @@ val raw_print : bool ref
 (* Univ print flag, never set anywere. Maybe should belong to Univ? *)
 val univ_print : bool ref
 
-type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | 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
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 16fe40555..33b032704 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -126,7 +126,7 @@ let init_ocaml_path () =
     Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir Coq_config.all_src_dirs
 
-let get_compat_version = function
+let get_compat_version ?(allow_old = true) = function
   | "8.7" -> Flags.Current
   | "8.6" -> Flags.V8_6
   | "8.5" -> Flags.V8_5
@@ -134,6 +134,7 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
+    if allow_old then Flags.VOld else
     CErrors.user_err ~hdr:"get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
   | s -> CErrors.user_err ~hdr:"get_compat_version"
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 3b42289ee..787dfb61a 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -25,4 +25,4 @@ val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
 
-val get_compat_version : string -> Flags.compat_version
+val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 31450ebd5..7a487f809 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -514,7 +514,9 @@ let parse_args arglist =
     |"-async-proofs-delegation-threshold" ->
         Flags.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
-    |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
+    |"-compat" ->
+        let v = get_compat_version ~allow_old:false (next ()) in
+        Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true