Qualified ML tactic names. The plugin name is used to discriminate

potentially conflicting tactics names from different plugins.

12 files changed, 60 insertions, 28 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 5df373d589..9631ed95e7 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -21,6 +21,8 @@ open Compat
 
 let dloc = <:expr< Loc.ghost >>
 
+let plugin_name = <:expr< __coq_plugin_name >>
+
 let rec make_patt = function
   | [] -> <:patt< [] >>
   | GramNonTerminal(loc',_,_,Some p)::l ->
@@ -182,7 +184,8 @@ let declare_tactic loc s c cl = match cl with
   let patt = make_patt rem in
   let vars = make_vars (List.length rem) in
   let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
-  let se = mlexpr_of_string s in
+  let entry = mlexpr_of_string s in
+  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let name = mlexpr_of_string name in
   let tac =
     (** Special handling of tactics without arguments: such tactics do not do
@@ -204,17 +207,18 @@ let declare_tactic loc s c cl = match cl with
       let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in
       try do {
         Tacenv.register_ml_tactic $se$ $tac$;
-        Mltop.declare_cache_obj obj __coq_plugin_name; }
+        Mltop.declare_cache_obj obj $plugin_name$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app
-            (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
             (Errors.print e)) ]; } >>
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
       TacExtend tactic. *)
-  let se = mlexpr_of_string s in
+  let entry = mlexpr_of_string s in
+  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let pp = make_printing_rule se cl in
   let gl = mlexpr_of_clause cl in
   let atom =
@@ -225,12 +229,12 @@ let declare_tactic loc s c cl = match cl with
     [ <:str_item< do {
       try do {
         Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
-        Mltop.declare_cache_obj $obj$ __coq_plugin_name;
+        Mltop.declare_cache_obj $obj$ $plugin_name$;
         List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app
-            (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
             (Errors.print e)) ]; } >>
     ]
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 609ee2f369..1375552c32 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -83,6 +83,11 @@ type ('a,'t) match_rule =
   | Pat of 'a match_context_hyps list * 'a match_pattern * 't
   | All of 't
 
+type ml_tactic_name = {
+  mltac_plugin : string;
+  mltac_tactic : string;
+}
+
 (** Composite types *)
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
@@ -157,7 +162,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
   (* For ML extensions *)
-  | TacExtend of Loc.t * string * 'lev generic_argument list
+  | TacExtend of Loc.t * ml_tactic_name * 'lev generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index fac81cdceb..e8072aa1a4 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -252,7 +252,7 @@ type tactic_grammar = {
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
   | TacticGrammar of KerName.t * tactic_grammar
-  | MLTacticGrammar of string * grammar_prod_item list list
+  | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list
 
 (** ML Tactic grammar extensions *)
 
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index b51c19f7a5..2a5e89eb93 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -50,7 +50,7 @@ val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
 (** Add a tactic notation rule to the parsing system. This produces a TacAlias
     tactic with the provided kernel name. *)
 
-val extend_ml_tactic_grammar : string -> grammar_prod_item list list -> unit
+val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit
 (** Add a ML tactic notation rule to the parsing system. This produces a
     TacExtend tactic with the provided string as name. *)
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8d83ffc330..18be9b2282 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -139,9 +139,13 @@ let closed_term_ast l =
    Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
 *)
 let closed_term_ast l =
+  let tacname = {
+    mltac_plugin = "newring_plugin";
+    mltac_tactic = "closed_term";
+  } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
-  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,tacname,
   [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
    Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])))
 (*
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 04e1a49232..381534d6da 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -260,7 +260,12 @@ let pr_extend_gen pr_gen lev s l =
     let p = pr_tacarg_using_rule pr_gen (pl,l) in
     if lev' > lev then surround p else p
   with Not_found ->
-    str "<" ++ str s ++ str ">" ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+    let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+    let args = match l with
+    | [] -> mt ()
+    | _ -> spc() ++ pr_sequence pr_gen l
+    in
+    str "<" ++ name ++ str ">" ++ args
 
 let pr_alias_gen pr_gen lev key l =
   try
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 82cb9c0a58..6c2f43cb68 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -51,7 +51,7 @@ type pp_tactic = {
   pptac_prods : int * grammar_terminals;
 }
 
-val declare_ml_tactic_pprule : string -> pp_tactic -> unit
+val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_clauses :  bool option ->
@@ -83,19 +83,19 @@ val pr_raw_extend:
   (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
   (tolerability -> raw_tactic_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) -> int ->
-    string -> raw_generic_argument list -> std_ppcmds
+  ml_tactic_name -> raw_generic_argument list -> std_ppcmds
 
 val pr_glob_extend:
   (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
   (tolerability -> glob_tactic_expr -> std_ppcmds) ->
   (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
-    string -> glob_generic_argument list -> std_ppcmds
+  ml_tactic_name -> glob_generic_argument list -> std_ppcmds
 
 val pr_extend :
   (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
   (tolerability -> glob_tactic_expr -> std_ppcmds) ->
   (constr_pattern -> std_ppcmds) -> int ->
-    string -> typed_generic_argument list -> std_ppcmds
+  ml_tactic_name -> typed_generic_argument list -> std_ppcmds
 
 val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
 
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 073df91cfa..94a9d03dcd 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -31,25 +31,39 @@ let interp_alias key =
 type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
 
-let tac_tab = Hashtbl.create 17
+module MLName =
+struct
+  type t = ml_tactic_name
+  let compare tac1 tac2 =
+    let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+    if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+    else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let pr_tacname t =
+  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+
+let tac_tab = ref MLTacMap.empty
 
 let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
   let () =
-    if Hashtbl.mem tac_tab s then
+    if MLTacMap.mem s !tac_tab then
       if overwrite then
-        let () = Hashtbl.remove tac_tab s in
-        msg_warning (str ("Overwriting definition of tactic " ^ s))
+        let () = tac_tab := MLTacMap.remove s !tac_tab in
+        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ s ^ "."))
+        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
   in
-  Hashtbl.add tac_tab s t
+  tac_tab := MLTacMap.add s t !tac_tab
 
 let interp_ml_tactic s =
   try
-    Hashtbl.find tac_tab s
+    MLTacMap.find s !tac_tab
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str s ++ str " is not installed.")
+      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
 
 let () =
   let assert_installed opn = let _ = interp_ml_tactic opn in () in
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index a7609ae215..4d64a5bb2b 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -45,8 +45,8 @@ type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
 (** Type of external tactics, used by [TacExtend]. *)
 
-val register_ml_tactic : ?overwrite:bool -> string -> ml_tactic -> unit
+val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
 (** Register an external tactic. *)
 
-val interp_ml_tactic : string -> ml_tactic
+val interp_ml_tactic : ml_tactic_name -> ml_tactic
 (** Get the named tactic. Raises a user error if it does not exist. *)
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 22588fcf16..84e5782f8d 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -63,7 +63,7 @@ val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
 val dump_glob_red_expr : raw_red_expr -> unit
 
 (* Hooks *)
-val assert_tactic_installed_hook : (string -> unit) Hook.t
+val assert_tactic_installed_hook : (ml_tactic_name -> unit) Hook.t
 val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t
 val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t
 val strict_check : bool ref
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6f6bfc52e7..fb1e0391b5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -128,7 +128,7 @@ let add_tactic_notation (local,n,prods,e) =
 type atomic_entry = string * Genarg.glob_generic_argument list option
 
 type ml_tactic_grammar_obj = {
-  mltacobj_name : string;
+  mltacobj_name : Tacexpr.ml_tactic_name;
   (** ML-side unique name *)
   mltacobj_prod : grammar_prod_item list list;
   (** Grammar rules generating the ML tactic. *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 326af7bba2..f48c4a700c 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -23,7 +23,7 @@ val add_tactic_notation :
 
 type atomic_entry = string * Genarg.glob_generic_argument list option
 
-val add_ml_tactic_notation : string ->
+val add_ml_tactic_notation : ml_tactic_name ->
   Egramml.grammar_prod_item list list -> atomic_entry list -> unit
 
 (** Adding a (constr) notation in the environment*)