diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-20 16:03:57 +0100 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-02 23:45:51 +0100 |
commit | 3ce123f16ce19f67dde4a0f3f2874a2678649907 (patch) | |
tree | 1357c6556ba947f066c16a1aa946c7e2ddb399d4 /parsing | |
parent | a4817d25befc71b7dbf707637660431144985133 (diff) |
Remove 8.5 compatibility support.
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6193ceb1a..4d6741ff5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -56,8 +56,7 @@ 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 -> + | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> |