Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable

2 files changed, 29 insertions, 0 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 958a205a1..a97ae8f65 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -369,9 +369,36 @@ module New = struct
     tclTHENSFIRSTn t1 l (tclUNIT())
   let tclTHENFIRST t1 t2 =
     tclTHENFIRSTn t1 [|t2|]
+
+  let tclBINDFIRST t1 t2 =
+    t1 >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+    match gls with
+    | [] -> tclFAIL 0 (str "Expect at least one goal.")
+    | hd::tl ->
+    Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans ->
+    Proofview.Unsafe.tclNEWGOALS tl <*>
+    Proofview.tclUNIT ans
+
   let tclTHENLASTn t1 l =
     tclTHENS3PARTS t1 [||] (tclUNIT()) l
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
+
+  let option_of_failure f x = try Some (f x) with Failure _ -> None
+
+  let tclBINDLAST t1 t2 =
+    t1 >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+    match option_of_failure List.sep_last gls with
+    | None -> tclFAIL 0 (str "Expect at least one goal.")
+    | Some (last,firstn) ->
+    Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun newgls ->
+    tclEVARMAP >>= fun sigma ->
+    let firstn = Proofview.Unsafe.undefined sigma firstn in
+    Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*>
+    Proofview.tclUNIT ans
+
   let tclTHENS t l =
     tclINDEPENDENT begin
       t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f0ebac780..340d8fbf3 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -196,8 +196,10 @@ module New : sig
   (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls]
       and [tac2] to the first resulting subgoal *)
   val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
+  val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
   val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic
   val tclTHENLAST  : unit tactic -> unit tactic -> unit tactic
+  val tclBINDLAST  : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
   (* [tclTHENS t l = t <*> tclDISPATCH l] *)
   val tclTHENS : unit tactic -> unit tactic list -> unit tactic
   (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *)