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 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/tac2stdlib.ml')

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