aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index f5b3f4e007..afdbe0c0dc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -35,7 +35,7 @@ struct
let hash = String.hash
let check_valid ?(strict=true) x =
- let iter (fatal, x) = if fatal || strict then CErrors.error x in
+ let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in
Option.iter iter (Unicode.ident_refutation x)
let is_valid s = match Unicode.ident_refutation s with