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.

4 files changed, 13 insertions, 63 deletions

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