Tactics declared through TACTIC EXTEND that are of the form

"foobar" constr(x1) ... constr(xn)

are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.

4 files changed, 71 insertions, 56 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 5a65fe93a3..3afbc8138e 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -10,6 +10,7 @@
 
 open Util
 open Pp
+open Names
 open Genarg
 open Q_util
 open Q_coqast
@@ -56,6 +57,8 @@ let rec extract_signature = function
   | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
   | _::l -> extract_signature l
 
+
+
 let check_unicity s l =
   let l' = List.map (fun (l,_,_) -> extract_signature l) l in
   if not (Util.List.distinct l') then
@@ -159,20 +162,39 @@ let possibly_atomic loc prods =
   in
   possibly_empty_subentries loc (List.factorize_left String.equal l)
 
+(** Special treatment of constr entries *)
+let is_constr_gram = function
+| GramTerminal _ -> false
+| GramNonTerminal (_, _, e, _) ->
+  match e with
+  | Aentry ("constr", "constr") -> true
+  | _ -> false
+
+let make_vars len =
+  (** We choose names unlikely to be written by a human, even though that
+      does not matter at all. *)
+  List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i)))
+
 let declare_tactic loc s c cl = match cl with
-| [[GramTerminal name], _, tac] ->
-  (** The extension is only made of a name: we do not add any grammar nor
-      printing rule and add it as a true Ltac definition. *)
+| [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
+  (** The extension is only made of a name followed by constr entries: we do not
+      add any grammar nor printing rule and add it as a true Ltac definition. *)
+  let patt = make_patt rem in
+  let vars = make_vars (List.length rem) in
+  let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
   let se = mlexpr_of_string s in
   let name = mlexpr_of_string name in
-  let tac = <:expr< fun _ $lid:"ist"$ -> $tac$ >> in
-  let body = <:expr< Tacexpr.TacAtom ($dloc$, Tacexpr.TacExtend($dloc$, $se$, [])) >> in
+  let tac = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+  (** Arguments are not passed directly to the ML tactic in the TacExtend 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.TacAtom ($dloc$, Tacexpr.TacExtend($dloc$, $se$, []))) >> in
   let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in
   declare_str_items loc
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in
       try do {
-        Tacenv.register_ml_tactic $se$ $tac$;
+        Tacenv.register_ml_tactic $se$ (Tacinterp.lift_constr_tac_to_ml_tac $vars$ $tac$);
         Mltop.declare_cache_obj obj __coq_plugin_name; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 2434d3f453..d3b9dd1325 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -23,58 +23,26 @@ TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
 
-let make_vars len =
-  List.init len (fun i -> Id.of_string (Printf.sprintf "_%i" i))
-
-let dummy_id = Id.of_string "_"
-
-(** Add a tactic that only uses constrs arguments. Such tactics actually do
-    not need to define grammar rules, because tactic arguments are already
-    parsed as constrs. So we add them manually. *)
-(** TODO: do this automagically in TACTIC EXTEND and use it in this file *)
-let add_constr_tactic name len tac =
-  let vars = make_vars len in
-  (** We pass the arguments through the environment rather than through the
-      tactic, to overcome the way tactics arguments are interpreted. *)
-  let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let map id =
-      let c = Id.Map.find id ist.lfun in
-      try Taccoerce.coerce_to_closed_constr env c
-      with Taccoerce.CannotCoerceTo ty ->
-        error_ltac_variable Loc.ghost dummy_id (Some env) c ty
-    in
-    let args = List.map map vars in
-    tac args ist
-  end in
-  let () = Tacenv.register_ml_tactic name tac in
-  let ref = Libnames.Ident (Loc.ghost, Id.of_string name) in
-  let args = List.map (fun id -> Some id) vars in
-  let body = TacExtend (Loc.ghost, name, []) in
-  let body = TacFun (args, TacAtom (Loc.ghost, body)) in
-  let obj () = Tacenv.register_ltac false false [ref, false, body] in
-  Mltop.declare_cache_obj obj "coretactics"
-
-let () =
-  let tac args _ = match args with [c] _ -> Tactics.cut c | _ -> assert false in
-  add_constr_tactic "cut" 1 tac
+TACTIC EXTEND cut
+  [ "cut" constr(c) ] -> [ Tactics.cut c ]
+END
 
-let () =
-  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.exact_no_check c) | _ -> assert false in
-  add_constr_tactic "exact_no_check" 1 tac
+TACTIC EXTEND exact_no_check
+  [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+END
 
-let () =
-  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.vm_cast_no_check c) | _ -> assert false in
-  add_constr_tactic "vm_cast_no_check" 1 tac
+TACTIC EXTEND vm_cast_no_check
+  [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ]
+END
 
-let () =
-  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.case_type c) | _ -> assert false in
-  add_constr_tactic "casetype" 1 tac
+TACTIC EXTEND casetype
+  [ "casetype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.case_type c) ]
+END
 
-let () =
-  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.elim_type c) | _ -> assert false in
-  add_constr_tactic "elimtype" 1 tac
+TACTIC EXTEND elimtype
+  [ "elimtype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.elim_type c) ]
+END
 
-let () =
-  let tac args _ = match args with [c] -> Tactics.cut_and_apply c | _ -> assert false in
-  add_constr_tactic "lapply" 1 tac
+TACTIC EXTEND lapply
+  [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
+END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4333c5696d..a992c52ce1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2109,3 +2109,23 @@ let _ = Hook.set Auto.extern_interp
     let lfun = Id.Map.map (fun c -> Value.of_constr c) l in
     let ist = { (default_ist ()) with lfun; } in
     interp_tactic ist)
+
+(** Used in tactic extension **)
+
+let dummy_id = Id.of_string "_"
+
+let lift_constr_tac_to_ml_tac vars tac =
+  let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let map = function
+    | None -> None
+    | Some id ->
+      let c = Id.Map.find id ist.lfun in
+      try Some (coerce_to_closed_constr env c)
+      with CannotCoerceTo ty ->
+        error_ltac_variable Loc.ghost dummy_id (Some env) c ty
+    in
+    let args = List.map_filter map vars in
+    tac args ist
+  end in
+  tac
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 090fb1ccab..71721427a7 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -113,3 +113,8 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t
 val interp_int : interp_sign -> Id.t Loc.located -> int
 
 val error_ltac_variable : Loc.t -> Id.t -> Environ.env option -> value -> string -> 'a
+
+(** Transforms a constr-expecting tactic into a tactic finding its arguments in
+    the Ltac environment according to the given names. *)
+val lift_constr_tac_to_ml_tac : Id.t option list ->
+  (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic