aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 65c5917b7..50a228050 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -135,6 +135,7 @@ let get_compat_version = function
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
- Flags.V8_2
- | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
+ Errors.errorlabstrm "get_compat_version"
+ (str "Compatibility with version " ++ str s ++ str " not supported.")
+ | s -> Errors.errorlabstrm "get_compat_version"
+ (str "Unknown compatibility version \"" ++ str s ++ str "\".")