From 1c55826018c5f07ee25b5771e59fe0389293cb62 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 31 Jul 2017 14:06:02 +0200 Subject: [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. --- toplevel/coqinit.ml | 12 ------------ toplevel/coqinit.mli | 2 -- toplevel/coqtop.ml | 2 +- 3 files changed, 1 insertion(+), 15 deletions(-) (limited to 'toplevel') 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 ()) -- cgit v1.2.3