aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-02-20 16:03:57 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-02 23:45:51 +0100
commit3ce123f16ce19f67dde4a0f3f2874a2678649907 (patch)
tree1357c6556ba947f066c16a1aa946c7e2ddb399d4 /parsing
parenta4817d25befc71b7dbf707637660431144985133 (diff)
Remove 8.5 compatibility support.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml43
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 ->