Binding the specialize tactic.

6 files changed, 34 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 60b6e70d58..6026b5b319 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -569,6 +569,12 @@ let () = define_prim3 "tac_constructorn" begin fun ev n bnd ->
   Tac2tactics.constructor_tac ev None n bnd
 end
 
+let () = define_prim2 "tac_specialize" begin fun c ipat ->
+  let c = to_constr_with_bindings c in
+  let ipat = Value.to_option to_intro_pattern ipat in
+  Tac2tactics.specialize c ipat
+end
+
 let () = define_prim1 "tac_symmetry" begin fun cl ->
   let cl = to_clause cl in
   Tac2tactics.symmetry cl
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index f7ad057e86..eec0d2ab45 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -150,6 +150,11 @@ let split_with_bindings ev bnd =
   let bnd = mk_bindings bnd in
   Tactics.split_with_bindings ev [bnd]
 
+let specialize c pat =
+  let c = mk_with_bindings c in
+  let pat = Option.map mk_intro_pattern pat in
+  Tactics.specialize c pat
+
 let change pat c cl =
   let open Tac2ffi in
   Proofview.Goal.enter begin fun gl ->
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 7a4624ba2c..96c7b9214c 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -38,6 +38,8 @@ val left_with_bindings  : evars_flag -> bindings -> unit tactic
 val right_with_bindings : evars_flag -> bindings -> unit tactic
 val split_with_bindings : evars_flag -> bindings -> unit tactic
 
+val specialize : constr_with_bindings -> intro_pattern option -> unit tactic
+
 val change : Pattern.constr_pattern option -> (constr array, constr) Tac2ffi.fun1 -> clause -> unit tactic
 
 val rewrite :
diff --git a/tests/example2.v b/tests/example2.v
index 46e4e43ed0..c953d25061 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -266,3 +266,16 @@ Proof.
 change (?a + 1 = 2) with (2 = $a + 1).
 reflexivity.
 Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl).
+destruct H.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl) as [].
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index dc09812254..f16a3a9161 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -204,6 +204,12 @@ Ltac2 Notation "econstructor" := Control.enter (fun () => Std.constructor true).
 Ltac2 Notation econstructor := econstructor.
 Ltac2 Notation "econstructor" n(tactic) bnd(thunk(with_bindings)) := constructor0 true n bnd.
 
+Ltac2 specialize0 c pat :=
+  enter_h false (fun _ c => Std.specialize c pat) c.
+
+Ltac2 Notation "specialize" c(thunk(seq(constr, with_bindings))) ipat(opt(seq("as", intropattern))) :=
+  specialize0 c ipat.
+
 Ltac2 elim0 ev c bnd use :=
   let f ev ((c, bnd, use)) := Std.elim ev (c, bnd) use in
   enter_h ev f (fun () => c (), bnd (), use ()).
diff --git a/theories/Std.v b/theories/Std.v
index 389299f266..73b2ba02c4 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -227,6 +227,8 @@ Ltac2 @ external move : ident -> move_location -> unit := "ltac2" "tac_move".
 
 Ltac2 @ external intro : ident option -> move_location option -> unit := "ltac2" "tac_intro".
 
+Ltac2 @ external specialize : constr_with_bindings -> intro_pattern option -> unit := "ltac2" "tac_specialize".
+
 (** extratactics *)
 
 Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "ltac2" "tac_discriminate".