From dfb64dda51f7eea174e41129c8d2e0c3559298ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Apr 2015 08:35:57 +0200
Subject: Fixing bug #4190.

The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
---
 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 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. *)
-- 
cgit v1.2.3