Embedding the index of the ML tactic entry in the Tacexpr AST.

This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.

9 files changed, 27 insertions, 10 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 0421ad7ce4..e91e666968 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -186,6 +186,7 @@ let declare_tactic loc s c cl = match cl with
   let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
   let entry = mlexpr_of_string s in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
+  let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
   let tac =
     (** Special handling of tactics without arguments: such tactics do not do
@@ -200,7 +201,7 @@ let declare_tactic loc s c cl = match cl with
   (** Arguments are not passed directly to the ML tactic in the TacML node,
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
-  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in
+  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in
   let name = <:expr< Names.Id.of_string $name$ >> in
   declare_str_items loc
     [ <:str_item< do {
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7b9ad3136b..f0377cff97 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -101,6 +101,11 @@ type ml_tactic_name = {
   mltac_tactic : string;
 }
 
+type ml_tactic_entry = {
+  mltac_name : ml_tactic_name;
+  mltac_index : int;
+}
+
 (** Composite types *)
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
@@ -287,7 +292,7 @@ and 'a gen_tactic_expr =
   | TacFun of 'a gen_tactic_fun_ast
   | TacArg of 'a gen_tactic_arg located
   (* For ML extensions *)
-  | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
+  | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
 
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 01194c60d0..d9eb5d4126 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -258,8 +258,12 @@ type all_grammar_command =
 
 let add_ml_tactic_entry name prods =
   let entry = weaken_entry Tactic.simple_tactic in
-  let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in
-  let rules = List.map (make_rule mkact) prods in
+  let mkact i loc l : raw_tactic_expr =
+    let open Tacexpr in
+    let entry = { mltac_name = name; mltac_index = i } in
+    TacML (loc, entry, List.map snd l)
+  in
+  let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
   synchronize_level_positions ();
   grammar_extend entry None (None ,[(None, None, List.rev rules)]);
   1
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509c2..72ebfae486 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -143,6 +143,10 @@ let closed_term_ast l =
     mltac_plugin = "newring_plugin";
     mltac_tactic = "closed_term";
   } in
+  let tacname = {
+    mltac_name = tacname;
+    mltac_index = 0;
+  } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8264e5af6..bc837d81de 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1250,7 +1250,7 @@ module Make
             | TacArg (_,a) ->
               pr_tacarg a, latom
             | TacML (loc,s,l) ->
-              pr_with_comments loc (pr.pr_extend 1 s l), lcall
+              pr_with_comments loc (pr.pr_extend 1 s.mltac_name 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/tactics/tacenv.ml b/tactics/tacenv.ml
index cb20fc9308..9d8b9a9d54 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -58,7 +58,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
-let interp_ml_tactic s =
+let interp_ml_tactic { mltac_name = s } =
   try
     MLTacMap.find s !tac_tab
   with Not_found ->
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 29677fd4ca..72b1ca90ff 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -51,5 +51,5 @@ type ml_tactic =
 val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
 (** Register an external tactic. *)
 
-val interp_ml_tactic : ml_tactic_name -> ml_tactic
+val interp_ml_tactic : ml_tactic_entry -> ml_tactic
 (** Get the named tactic. Raises a user error if it does not exist. *)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4b03ff249f..8de804d6dc 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -159,6 +159,7 @@ let flatten_contravariant_conj flags ist =
 
 let constructor i =
   let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
+  let name = { Tacexpr.mltac_name = name; mltac_index = 0 } in
   let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
   Tacexpr.TacML (Loc.ghost, name, [i])
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 161cf82470..968f72486a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -137,13 +137,15 @@ type ml_tactic_grammar_obj = {
 (** ML tactic notations whose use can be restricted to an identifier are added
     as true Ltac entries. *)
 let extend_atomic_tactic name entries =
-  let add_atomic (id, args) = match args with
+  let add_atomic i (id, args) = match args with
   | None -> ()
   | Some args ->
-    let body = Tacexpr.TacML (Loc.ghost, name, args) in
+    let open Tacexpr in
+    let entry = { mltac_name = name; mltac_index = i } in
+    let body = TacML (Loc.ghost, entry, args) in
     Tacenv.register_ltac false false (Names.Id.of_string id) body
   in
-  List.iter add_atomic entries
+  List.iteri add_atomic entries
 
 let cache_ml_tactic_notation (_, obj) =
   extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod