aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d9cd574a0..59ee95b31 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -136,7 +136,7 @@ let get_compat_version = function
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- CErrors.errorlabstrm "get_compat_version"
+ CErrors.user_err ~hdr:"get_compat_version"
(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s -> CErrors.errorlabstrm "get_compat_version"
+ | s -> CErrors.user_err ~hdr:"get_compat_version"
(str "Unknown compatibility version \"" ++ str s ++ str "\".")