2 files changed, 12 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 4ccf5b60ae..480b37e897 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -33,9 +33,9 @@ struct
 
   let hash = String.hash
 
-  let check_soft x =
+  let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
@@ -48,6 +48,11 @@ struct
     let s = String.copy s in
     String.hcons s
 
+  let of_string_soft s =
+    let () = check_soft ~warn:false s in
+    let s = String.copy s in
+    String.hcons s
+
   let to_string id = String.copy id
 
   let print id = str id
diff --git a/kernel/names.mli b/kernel/names.mli
index d82043da1a..92ee58f260 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -29,7 +29,11 @@ sig
 
   val of_string : string -> t
   (** Converts a string into an identifier. May raise [UserError _] if the
-      string is not valid. *)
+      string is not valid, or echo a warning if it contains invalid identifier
+      characters. *)
+
+  val of_string_soft : string -> t
+  (** Same as {!of_string} except that no warning is ever issued. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)