[general] Remove spurious dependency of highparsing on toplevel.

`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.

This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.

5 files changed, 17 insertions, 18 deletions

diff --git a/Makefile.common b/Makefile.common
index 85ecb1a08..2e24ac8e9 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -105,7 +105,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
-	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma API/API.cma
+	parsing/highparsing.cma stm/stm.cma toplevel/toplevel.cma API/API.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d29fca77..99c8b1dbf 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -51,6 +51,19 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+let parse_compat_version ?(allow_old = true) = let open Flags in function
+  | "8.8" -> Current
+  | "8.7" -> V8_7
+  | "8.6" -> V8_6
+  | "8.5" -> V8_5
+  | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+    if allow_old then VOld else
+    CErrors.user_err ~hdr:"get_compat_version"
+      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
+  | s ->
+    CErrors.user_err ~hdr:"get_compat_version"
+      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
+
 let extraction_err ~loc =
   if not (Mltop.module_is_known "extraction_plugin") then
     CErrors.user_err ~loc (str "Please do first a Require Extraction.")
@@ -1163,7 +1176,7 @@ GEXTEND Gram
     [ [ "("; IDENT "only"; IDENT "parsing"; ")" ->
          Some Flags.Current
       | "("; IDENT "compat"; s = STRING; ")" ->
-         Some (Coqinit.get_compat_version s)
+         Some (parse_compat_version s)
       | -> None ] ]
   ;
   obsolete_locality:
@@ -1181,7 +1194,7 @@ GEXTEND Gram
       | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
       | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
       | IDENT "compat"; s = STRING ->
-        SetCompatVersion (Coqinit.get_compat_version s)
+        SetCompatVersion (parse_compat_version s)
       | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s];
                         s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] ->
           begin match s1, s2 with
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 326ef5471..5ca886965 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -125,15 +125,3 @@ let init_ocaml_path () =
   in
     Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir Coq_config.all_src_dirs
-
-let get_compat_version ?(allow_old = true) = function
-  | "8.8" -> Flags.Current
-  | "8.7" -> Flags.V8_7
-  | "8.6" -> Flags.V8_6
-  | "8.5" -> Flags.V8_5
-  | ("8.4" | "8.3" | "8.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"
-      (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index bf8558d10..3432e79cc 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -24,5 +24,3 @@ val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
-
-val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 515552fe7..5ecd71a39 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -518,7 +518,7 @@ let parse_args arglist =
         Flags.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" ->
-        let v = get_compat_version ~allow_old:false (next ()) in
+        let v = G_vernac.parse_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 ())