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.

1 files changed, 13 insertions, 5 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c8eff59b1..639ec1e6e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -62,11 +62,19 @@ let rec make_tags = function
   | [] -> []
 
 let make_fresh_key =
-  let id = Summary.ref ~name:"Tactic Notation counter" 0 in
-  fun () -> KerName.make
-    (Safe_typing.current_modpath (Global.safe_env ()))
-    (Global.current_dirpath ())
-    (incr id; Label.make ("_" ^ string_of_int !id))
+  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
 
 type tactic_grammar_obj = {
   tacobj_key : KerName.t;