More primitive tactics.

2 files changed, 19 insertions, 0 deletions

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
diff --git a/theories/Std.v b/theories/Std.v
index a27790c35d..d2b85f215e 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -83,6 +83,9 @@ Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
 
 Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".
 
+Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_assert".
+Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough".
+
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
 Ltac2 @ external set : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
 Ltac2 @ external eset : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_eset".