diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-31 14:06:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-31 14:06:02 +0200 |
| commit | 1c55826018c5f07ee25b5771e59fe0389293cb62 (patch) | |
| tree | 7e9f641d39a29e5848c4e8bc90b9702dc793c899 /toplevel/coqinit.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
[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.
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 12 |
1 files changed, 0 insertions, 12 deletions
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 "\".") |