diff options
| author | Théo Zimmermann | 2019-11-13 15:50:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-02 17:23:22 +0100 |
| commit | 88fe0bcf86ad6cb95ffacfcd37f51fa3ae2da4fc (patch) | |
| tree | 05a0ed1f5d31789ea0457fe6caf5df0c95050c5e /toplevel | |
| parent | fcf5d724b5bd26581ecad6055ee33d2758133854 (diff) | |
Remove deprecated compat modifier of Notation / Infix commands.
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index e3116550d9..5326ce6114 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -174,13 +174,6 @@ let add_vo_include opts unix_path coq_path implicit = let add_vo_require opts d p export = { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} -let add_compat_require opts v = - match v with - | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) - | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) - | Flags.V8_11 -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq812" None (Some false) - let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} @@ -274,6 +267,18 @@ let get_native_name s = Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" +let get_compat_file = function + | "8.12" -> "Coq.Compat.Coq812" + | "8.11" -> "Coq.Compat.Coq811" + | "8.10" -> "Coq.Compat.Coq810" + | "8.9" -> "Coq.Compat.Coq89" + | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + let to_opt_key = Str.(split (regexp " +")) let parse_option_set opt = @@ -379,9 +384,7 @@ let parse_args ~help ~init arglist : t * string list = |"-worker-id" -> set_worker_id opt (next ()); oval |"-compat" -> - let v = G_vernac.parse_compat_version (next ()) in - Flags.compat_version := v; - add_compat_require oval v + add_vo_require oval (get_compat_file (next ())) None (Some false) |"-exclude-dir" -> System.exclude_directory (next ()); oval |