From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 kernel/names.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index d82043da..92ee58f2 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. *)
-- 
cgit v1.2.3