External tactics and notations now accept any tactic argument.

This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.

I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.

There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.

Also fixes bug #3849 en passant.

1 files changed, 20 insertions, 2 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 84736f8aba..2bc5b0f83f 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -257,7 +257,8 @@ let add_ml_tactic_entry name prods =
   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)
+    let map (_, arg) = TacGeneric arg in
+    TacML (loc, entry, List.map map l)
   in
   let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
   synchronize_level_positions ();
@@ -274,7 +275,24 @@ let head_is_ident tg = match tg.tacgram_prods with
 
 let add_tactic_entry kn tg =
   let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in
+  let mkact loc l =
+    let filter = function
+    | GramTerminal _ -> None
+    | GramNonTerminal (_, t, _, None) -> None
+    | GramNonTerminal (_, t, _, Some _) -> Some (Genarg.unquote t)
+    in
+    let types = List.map_filter filter tg.tacgram_prods in
+    let map (id, arg) t =
+      (** HACK to handle especially the tactic(...) entry *)
+      let wit = Genarg.rawwit Constrarg.wit_tactic in
+      if Genarg.argument_type_eq t (Genarg.unquote wit) then
+        (id, Tacexp (Genarg.out_gen wit arg))
+      else
+        (id, TacGeneric arg)
+    in
+    let l = List.map2 map l types in
+    (TacAlias (loc,kn,l):raw_tactic_expr)
+  in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
       error "Notation for simple tactic must start with an identifier."