Splitting ML tactics in one function per grammar entry.

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

1 files changed, 10 insertions, 9 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e91e666968..5cf23067af 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -75,7 +75,8 @@ let make_clause (pt,_,e) =
 
 let make_fun_clauses loc s l =
   check_unicity s l;
-  Compat.make_fun loc (List.map make_clause l)
+  let map c = Compat.make_fun loc [make_clause c] in
+  mlexpr_of_list map l
 
 let rec make_args = function
   | [] -> <:expr< [] >>
@@ -110,14 +111,14 @@ let rec make_tags loc = function
       <:expr< [ $t$ :: $l$ ] >>
   | _::l -> make_tags loc l
 
-let make_one_printing_rule se (pt,_,e) =
+let make_one_printing_rule (pt,_,e) =
   let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
   let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
-  <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$;
-            pptac_prods = ($level$, $prods$) }) >>
+  <:expr< { Pptactic.pptac_args = $make_tags loc pt$;
+            pptac_prods = ($level$, $prods$) } >>
 
-let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
+let make_printing_rule = mlexpr_of_list make_one_printing_rule
 
 let make_empty_check = function
 | GramNonTerminal(_, t, e, _)->
@@ -207,7 +208,7 @@ let declare_tactic loc s c cl = match cl with
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac True False $name$ $body$ in
       try do {
-        Tacenv.register_ml_tactic $se$ $tac$;
+        Tacenv.register_ml_tactic $se$ [|$tac$|];
         Mltop.declare_cache_obj obj $plugin_name$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
@@ -220,7 +221,7 @@ let declare_tactic loc s c cl = match cl with
       TacML tactic. *)
   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 pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let atom =
     mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
@@ -229,9 +230,9 @@ let declare_tactic loc s c cl = match cl with
   declare_str_items loc
     [ <:str_item< do {
       try do {
-        Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
+        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
         Mltop.declare_cache_obj $obj$ $plugin_name$;
-        List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
+        Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app