From dd1343eb2680c202cf059e3db5788904b7d79782 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 21:52:15 +0200
Subject: More primitive tactics.

---
 src/tac2stdlib.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'src/tac2stdlib.ml')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 44fad48955..8fdf9c6d8c 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -196,6 +196,22 @@ let () = define_prim1 "tac_egeneralize" begin fun cl ->
   Tactics.new_generalize_gen cl
 end
 
+let () = define_prim3 "tac_assert" begin fun c tac ipat ->
+  let c = Value.to_constr c in
+  let of_tac t = Proofview.tclIGNORE (thaw t) in
+  let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
+  let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
+  Tactics.forward true tac ipat c
+end
+
+let () = define_prim3 "tac_enough" begin fun c tac ipat ->
+  let c = Value.to_constr c in
+  let of_tac t = Proofview.tclIGNORE (thaw t) in
+  let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
+  let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
+  Tactics.forward false tac ipat c
+end
+
 let () = define_prim2 "tac_pose" begin fun idopt c ->
   let na = to_name idopt in
   let c = Value.to_constr c in
-- 
cgit v1.2.3