From 00853ca988d304af5b41834ee6b5766532233349 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 4 Feb 2015 14:31:57 +0100
Subject: Tactic Notation: use stable unique key for notations (Close: 3970)

---
 toplevel/metasyntax.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 161cf82470..9d7baa21d2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -68,16 +68,24 @@ type tactic_grammar_obj = {
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
-let cache_tactic_notation ((_, key), tobj) =
+let key k tobj =
+  let mp,dp,_ = KerName.repr k in
+  KerName.make mp dp
+    (Label.make ("_" ^ string_of_int (Hashtbl.hash tobj.tacobj_tacgram)))
+
+let cache_tactic_notation ((_,k), tobj) =
+  let key = key k tobj in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
-let open_tactic_notation i ((_, key), tobj) =
+let open_tactic_notation i ((_,k), tobj) =
+  let key = key k tobj in
   if Int.equal i 1 && not tobj.tacobj_local then
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
-let load_tactic_notation i ((_, key), tobj) =
+let load_tactic_notation i ((_,k), tobj) =
+  let key = key k tobj in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
-- 
cgit v1.2.3