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.

3 files changed, 43 insertions, 50 deletions

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