diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 11:52:19 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 11:52:19 +0200 |
| commit | 28c732ea340f5ac571a77a8ac26de600c29165b2 (patch) | |
| tree | 9ee6deb6ecb31c520ffb4c278560a527cb550db4 /toplevel | |
| parent | e710306910afc61c9a874e6020bbf35b77ffe4af (diff) | |
| parent | 7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa (diff) | |
Merge PR#375: Deprecation
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 8 |
3 files changed, 9 insertions, 9 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 16fe40555..f36d0c348 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -126,14 +126,12 @@ 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 - | "8.4" -> Flags.V8_4 - | "8.3" -> Flags.V8_3 - | "8.2" -> Flags.V8_2 - | ("8.1" | "8.0") as s -> + | ("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" 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..5f0716fd9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -205,9 +205,9 @@ let require () = let add_compat_require v = match v with - | Flags.V8_4 -> add_require "Coq.Compat.Coq84" | Flags.V8_5 -> add_require "Coq.Compat.Coq85" - | _ -> () + | Flags.V8_6 -> add_require "Coq.Compat.Coq86" + | Flags.VOld | Flags.Current -> () let compile_list = ref ([] : (bool * string) list) @@ -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 |