From 8524f80ad30b744b66186cf59aec8d2524490da7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 3 Feb 2015 21:05:53 +0100
Subject: Revert "Tactic Notation: use stable unique key for notations (Close:
 3970)"

This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910.
---
 toplevel/metasyntax.ml | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6122294b54..161cf82470 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -61,34 +61,23 @@ let rec make_tags = function
   | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
   | [] -> []
 
-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))
-
 type tactic_grammar_obj = {
-  tacobj_key : KerName.t; 
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
-let cache_tactic_notation (_, tobj) =
-  let key = tobj.tacobj_key in
+let cache_tactic_notation ((_, key), tobj) =
   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 (_, tobj) =
-  let key = tobj.tacobj_key in
+let open_tactic_notation i ((_, key), tobj) =
   if Int.equal i 1 && not tobj.tacobj_local then
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
-let load_tactic_notation i (_, tobj) =
-  let key = tobj.tacobj_key in
+let load_tactic_notation i ((_, key), tobj) =
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
@@ -126,7 +115,6 @@ let add_tactic_notation (local,n,prods,e) =
     tacgram_prods = prods;
   } in
   let tacobj = {
-    tacobj_key = make_fresh_key ();
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;
-- 
cgit v1.2.3