Splitting ML tactics in one function per grammar entry.

Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.

3 files changed, 17 insertions, 12 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index bc837d81de..a76d73006a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -34,13 +34,14 @@ type pp_tactic = {
 }
 
 (* ML Extensions *)
-let prtac_tab = Hashtbl.create 17
+let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
+  Hashtbl.create 17
 
 (* Tactic notations *)
 let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
 
 let declare_ml_tactic_pprule key pt =
-  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+  Hashtbl.add prtac_tab key pt
 
 let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -414,14 +415,18 @@ module Make
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev s l =
+  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
     try
-      let tags = List.map genarg_tag l in
-      let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+      let pp_rules = Hashtbl.find prtac_tab s in
+      let pp = pp_rules.(i) in
+      let (lev', pl) = pp.pptac_prods in
       let p = pr_tacarg_using_rule pr_gen (pl,l) in
       if lev' > lev then surround p else p
     with Not_found ->
-      let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+      let name =
+        str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
+        str "@" ++ int i
+      in
       let args = match l with
         | [] -> mt ()
         | _ -> spc() ++ pr_sequence pr_gen l
@@ -756,7 +761,7 @@ module Make
     pr_reference : 'ref -> std_ppcmds;
     pr_name      : 'nam -> std_ppcmds;
     pr_generic   : 'lev generic_argument -> std_ppcmds;
-    pr_extend    : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
+    pr_extend    : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
     pr_alias     : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
   }
 
@@ -1250,7 +1255,7 @@ module Make
             | TacArg (_,a) ->
               pr_tacarg a, latom
             | TacML (loc,s,l) ->
-              pr_with_comments loc (pr.pr_extend 1 s.mltac_name l), lcall
+              pr_with_comments loc (pr.pr_extend 1 s l), lcall
             | TacAlias (loc,kn,l) ->
               pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
           )
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 284237f014..50cc4e2bc2 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -50,7 +50,7 @@ type pp_tactic = {
   pptac_prods : int * grammar_terminals;
 }
 
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit
+val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 98b5757daf..ee1669f7f8 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -60,19 +60,19 @@ module type Pp = sig
     (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
     (tolerability -> raw_tactic_expr -> std_ppcmds) ->
     (constr_expr -> std_ppcmds) -> int ->
-    ml_tactic_name -> raw_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> 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 ->
-    ml_tactic_name -> glob_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> 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 ->
-    ml_tactic_name -> typed_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
 
   val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds