Merge branch 'v8.5'

1 files changed, 5 insertions, 1 deletions

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. *)