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.

11 files changed, 76 insertions, 93 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index aa1088c9ea..6d10ef9d51 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -292,9 +292,9 @@ 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_entry * 'l generic_argument list
+  | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)
-  | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
+  | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list
 
 constraint 'a = <
     term:'t;
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."
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d596cf6fb8..88c8465b1b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -137,8 +137,8 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(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]))
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
@@ -228,7 +228,7 @@ let exec_tactic env evd n f args =
   (** Build the getter *)
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
-  let get_res = TacML (Loc.ghost, get_res, [n]) in
+  let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
   let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
   (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 6e051a1fc0..4cb7e9fb38 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -371,10 +371,11 @@ module Make
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+  let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
     try
       let pp_rules = Hashtbl.find prtac_tab s in
       let pp = pp_rules.(i) in
+      let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found 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
@@ -389,28 +390,35 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
-  let pr_alias_gen pr_gen lev key l =
+  let pr_alias_gen check pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
       let (lev', pl) = pp.pptac_prods in
+      let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
       let p = pr_tacarg_using_rule pr_gen (pl, l) in
       if lev' > lev then surround p else p
     with Not_found ->
       KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
+  let check_type t arg = match arg with
+  | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+  | _ -> false
+
+  let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
+
   let pr_raw_extend_rec prc prlc prtac prpat =
-    pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+    pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
   let pr_glob_extend_rec prc prlc prtac prpat =
-    pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat)
+    pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
   let pr_extend_rec prc prlc prtac prpat =
-    pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat)
+    pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
 
   let pr_raw_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+    pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
   let pr_glob_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat)
+    pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
   let pr_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat)
+    pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -716,8 +724,8 @@ module Make
     pr_reference : 'ref -> std_ppcmds;
     pr_name      : 'nam -> std_ppcmds;
     pr_generic   : 'lev generic_argument -> 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;
+    pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+    pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
   }
 
   constraint 'a = <
@@ -1352,9 +1360,18 @@ module Make
     (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
     (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
 
-  let pr_extend env = pr_extend_rec
-    (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-    (pr_glob_tactic_level env) pr_constr_pattern
+  let check_val_type t arg =
+    let t = Genarg.val_tag (Obj.magic t) in (** FIXME *)
+    let Val.Dyn (t', _) = arg in
+    match Genarg.Val.eq t t' with
+    | None -> false
+    | Some _ -> true
+
+  let pr_alias pr lev key args =
+    pr_alias_gen check_val_type pr lev key args
+
+  let pr_extend pr lev ml args =
+    pr_extend_gen check_val_type pr lev ml args
 
   let pr_tactic env = pr_tactic_level env ltop
 
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index d154e0b663..01f240f6b8 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -40,19 +40,16 @@ module type Pp = sig
   val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
 
   val pr_raw_extend: env -> int ->
-    ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
 
   val pr_glob_extend: env -> int ->
-    ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
 
-  val pr_extend : env -> int ->
-    ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
+  val pr_extend :
+    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
 
-  val pr_extend_gen :
-    ('a -> std_ppcmds) -> int -> ml_tactic_entry -> 'a list -> std_ppcmds
-
-  val pr_alias_gen : ('a -> std_ppcmds) ->
-    int -> Names.KerName.t -> 'a list -> std_ppcmds
+  val pr_alias : (Val.t -> std_ppcmds) ->
+    int -> Names.KerName.t -> Val.t list -> std_ppcmds
 
   val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 08d2d21a3f..93d64f686d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -656,11 +656,11 @@ and intern_tactic_seq onlytac ist = function
 
   (* For extensions *)
   | TacAlias (loc,s,l) ->
-      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
+      let l = List.map (fun (id,a) -> (id,intern_tacarg !strict_check false ist a)) l in
       ist.ltacvars, TacAlias (loc,s,l)
   | TacML (loc,opn,l) ->
       let _ignore = Tacenv.interp_ml_tactic opn in
-      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
+      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l)
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
@@ -700,7 +700,7 @@ and intern_tacarg strict onlytac ist = function
   | TacNumgoals -> TacNumgoals
   | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
   | TacGeneric arg ->
-    let (_, arg) = Genintern.generic_intern ist arg in
+    let arg = intern_genarg ist arg in
     TacGeneric arg
 
 (* Reads the rules of a Match Context or a Match *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5e5b2be243..1596406c9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -156,12 +156,7 @@ module Value = struct
 
 end
 
-let print_top_val env arg v =
-  let unpacker wit cst =
-    try val_cast (topwit wit) v; mt ()
-    with CastError _ -> mt ()
-  in
-  unpack { unpacker } arg
+let print_top_val env v = mt () (** FIXME *)
 
 let dloc = Loc.ghost
 
@@ -1244,51 +1239,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   (* For extensions *)
   | TacAlias (loc,s,l) ->
       let body = Tacenv.interp_alias s in
-      let rec f x = match genarg_tag x with
-      | ConstrArgType
-      | ListArgType ConstrArgType
-      | OptArgType _ | PairArgType _ -> (** generic handler *)
-        interp_genarg ist x
-      | _ as tag -> (** Special treatment. TODO: use generic handler  *)
-        Ftactic.nf_enter begin fun gl ->
-          let sigma = Tacmach.New.project gl in
-          let env = Proofview.Goal.env gl in
-          match tag with
-          | IdentArgType ->
-              Ftactic.return (value_of_ident (interp_ident ist env sigma
-                                               (Genarg.out_gen (glbwit wit_ident) x)))
-          | VarArgType ->
-              Ftactic.return (Value.of_constr (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)))
-          | ListArgType VarArgType ->
-              let wit = glbwit (wit_list wit_var) in
-              let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in
-              Ftactic.return (Value.of_list (val_tag wit_constr) ans)
-          | ListArgType IdentArgType ->
-              let wit = glbwit (wit_list wit_ident) in
-              let mk_ident x = intro_pattern_of_ident (interp_ident ist env sigma x) in
-              let ans = List.map mk_ident (Genarg.out_gen wit x) in
-              Ftactic.return (Value.of_list (val_tag wit_intro_pattern) ans)
-          | ListArgType t  ->
-              let open Ftactic in
-              list_unpack { list_unpacker = fun wit l ->
-                let map x = f (Genarg.in_gen (glbwit wit) x) in
-                Ftactic.List.map map (glb l) >>= fun l ->
-                let l = CList.map (fun x -> Value.cast (topwit wit) x) l in
-                Ftactic.return (Value.of_list (val_tag wit) l)
-              } x
-          | ExtraArgType _ ->
-              (** Special treatment of tactics *)
-              if Genarg.has_type x (glbwit wit_tactic) then
-                let tac = Genarg.out_gen (glbwit wit_tactic) x in
-                val_interp ist tac
-              else
-                Geninterp.generic_interp ist x
-          | _ -> assert false
-        end
-      in
       let (>>=) = Ftactic.bind in
       let interp_vars =
-        Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l
+        Ftactic.List.map (fun (x,v) -> interp_tacarg ist v >>= fun v -> Ftactic.return (x,v)) l
       in
       let addvar (x, v) accu = Id.Map.add x v accu in
       let tac l =
@@ -1302,8 +1255,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       in
       let tac =
         Ftactic.with_env interp_vars >>= fun (env, lr) ->
-        let l = List.map2 (fun (_, g) (_, t) -> print_top_val env g t) l lr in
-        let name () = Pptactic.pr_alias_gen (fun x -> x) 0 s l in
+        let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s (List.map snd lr) in
         Proofview.Trace.name_tactic name (tac lr)
       (* spiwack: this use of name_tactic is not robust to a
          change of implementation of [Ftactic]. In such a situation,
@@ -1316,10 +1268,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let trace = push_trace (loc,LtacMLCall tac) ist in
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       let tac = Tacenv.interp_ml_tactic opn in
-      let args = Ftactic.List.map_right (fun a -> interp_genarg ist a) l in
+      let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
       let tac args =
-        let l = List.map2 (print_top_val ()) l args in
-        let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in
+        let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
         Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
       in
       Ftactic.run args tac
@@ -1355,8 +1306,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
 
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
-  | TacGeneric arg ->
-      Geninterp.generic_interp ist arg
+  | TacGeneric arg -> interp_genarg ist arg
   | Reference r -> interp_ltac_reference dloc false ist r
   | ConstrMayEval c ->
       Ftactic.enter begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2132e9a573..45b2d317c2 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -245,8 +245,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   (* For extensions *)
   | TacAlias (_,s,l) ->
       let s = subst_kn subst s in
-      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
-  | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_genarg subst) l)
+      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_tacarg subst a)) l)
+  | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l)
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 
@@ -261,7 +261,7 @@ and subst_tacarg subst = function
   | TacPretype c -> TacPretype (subst_glob_constr subst c)
   | TacNumgoals -> TacNumgoals
   | Tacexp t -> Tacexp (subst_tactic subst t)
-  | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
+  | TacGeneric arg -> TacGeneric (subst_genarg subst arg)
 
 (* Reads the rules of a Match Context or a Match *)
 and subst_match_rule subst = function
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d84f471163..f0805f7d08 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -210,7 +210,7 @@ let constructor i =
   (** Take care of the index: this is the second entry in constructor. *)
   let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
   let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
-  Tacexpr.TacML (Loc.ghost, name, [i])
+  Tacexpr.TacML (Loc.ghost, name, [TacGeneric i])
 
 let is_disj _ ist =
   let flags = assoc_flags ist in
diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/closed/3849.v
index 5290054a06..a8dc3af9cf 100644
--- a/test-suite/bugs/opened/3849.v
+++ b/test-suite/bugs/closed/3849.v
@@ -5,4 +5,4 @@ Tactic Notation "bar" hyp_list(hs) := foo hs.
 Goal True.
 do 5 pose proof 0 as ?n0.
 foo n1 n2.
-Fail bar n3 n4.
+bar n3 n4.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7714cc8108..0f96c2b4af 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -171,6 +171,7 @@ let extend_atomic_tactic name entries =
   | None -> ()
   | Some args ->
     let open Tacexpr in
+    let args = List.map (fun a -> TacGeneric a) args 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