3 files changed, 34 insertions, 16 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3f02cf309..d5c42a04d 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) =
   Hashtbl.add prtac_tab_v7 (s,tags) prods;
   if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
 
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags)
+
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) -> 
     (constr_expr -> std_ppcmds) -> 
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 9e1555ce9..bd42a1ffe 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -53,6 +53,8 @@ type grammar_terminals = string option list
 val declare_extra_tactic_pprule : bool -> string -> 
   argument_type list * (int * grammar_terminals) -> unit
 
+val exists_extra_tactic_pprule : string -> argument_type list -> bool
+
 val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
 
 val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ad5ae7c60..8d4f3b83f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -88,22 +88,19 @@ let rec make_tags lev = function
       etyp :: make_tags lev l
   | [] -> []
 
-let declare_tactic_pprule n (s,l,tac) =
-  let pp = (make_tags n l, (n,List.map make_terminal_status l)) in
-  Pptactic.declare_extra_tactic_pprule true s pp;
-  Pptactic.declare_extra_tactic_pprule false s pp
+let declare_tactic_pprule n (s,t,p) =
+  Pptactic.declare_extra_tactic_pprule true s (t,p);
+  Pptactic.declare_extra_tactic_pprule false s (t,p)
 
-let cache_tactic_notation (_,(n,gl)) =
-  Egrammar.extend_grammar (Egrammar.TacticGrammar (n,gl));
-  List.iter (declare_tactic_pprule n) gl
+let cache_tactic_notation (_,((n,pa),pp)) =
+  Egrammar.extend_grammar (Egrammar.TacticGrammar (n,pa));
+  List.iter (declare_tactic_pprule n) pp
 
 let subst_one_tactic_notation subst (s,p,(d,tac)) =
   (s,p,(d,Tacinterp.subst_tactic subst tac))
 
-open Egrammar
-
-let subst_tactic_notation (_,subst,(n,g)) =
-  (n,List.map (subst_one_tactic_notation subst) g)
+let subst_tactic_notation (_,subst,((n,pa),pp)) =
+  ((n,List.map (subst_one_tactic_notation subst) pa),pp)
 
 let (inTacticGrammar, outTacticGrammar) =
   declare_object {(default_object "TacticGrammar") with
@@ -117,15 +114,32 @@ let cons_production_parameter l = function
   | VTerm _ -> l
   | VNonTerm (_,_,ido) -> option_cons ido l
 
-let locate_tactic_body dir (s,prods,e) = 
+let rec tactic_notation_key = function
+  | VTerm id :: _ -> id
+  | _ :: l -> tactic_notation_key l
+  | [] -> "terminal_free_notation"
+
+let rec next_key_away key t =
+  if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
+  else key
+
+let make_tactic_pprule n s prods =
+  let tags = make_tags n prods in
+  let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
+  (s, tags, (n,List.map make_terminal_status prods))
+
+let make_tactic_parule s prods e =
   let ids = List.fold_left cons_production_parameter [] prods in
   let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
-  (s,prods,(dir,tac))
+  (s,prods,(Lib.cwd (),tac))
+
+let locate_tactic_body n (s,prods,e) =
+  let (s',t,p as pp) = make_tactic_pprule n s prods in
+  (make_tactic_parule s' prods e, pp)
 
 let add_tactic_notation (n,g) =
-  let dir = Lib.cwd () in
-  let g = List.map (locate_tactic_body dir) g in
-  Lib.add_anonymous_leaf (inTacticGrammar (n,g))
+  let pa,pp = List.split (List.map (locate_tactic_body n) g) in
+  Lib.add_anonymous_leaf (inTacticGrammar ((n,pa),pp))
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)