diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/names.mli | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 976415e370..18f2ef0dee 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,7 +34,7 @@ struct let check_soft x = let iter (fatal, x) = - if fatal then error x else Pp.msg_warning (str x) + if fatal then Errors.error x else Pp.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/names.mli b/kernel/names.mli index 77d5ce8e61..96a7dff099 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -20,15 +20,16 @@ sig (** Comparison over identifiers *) val check : string -> unit - (** Check that a string may be converted to an identifier. Raise an exception - related to the problem when this is not the case. *) + (** Check that a string may be converted to an identifier. + Raise a [UserError _] exception related to the problem + when this is not the case. *) val check_soft : string -> unit (** As [check], but may raise a warning instead of failing when the string is not an identifier, but is a well-formed string. *) val of_string : string -> t - (** Converts a string into an identifier. *) + (** Converts a string into an identifier. May raise [UserError _] *) val to_string : t -> string (** Converts a identifier into an string. *) |