From 62606e17ff4afe6a897607d45471b7f4d3ef54b8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Nov 2017 11:41:49 +0100
Subject: Binding the specialize tactic.

---
 src/tac2stdlib.ml   | 6 ++++++
 src/tac2tactics.ml  | 5 +++++
 src/tac2tactics.mli | 2 ++
 3 files changed, 13 insertions(+)

(limited to 'src')

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 :
-- 
cgit v1.2.3