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