aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqinit.ml3
-rw-r--r--toplevel/coqtop.ml1
2 files changed, 1 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 4a17a5ee1..f36d0c348 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -130,8 +130,7 @@ 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" | "8.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.")
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7a487f809..3e4365605 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -205,7 +205,6 @@ 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"
| _ -> ()