2 files changed, 27 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..1d2c7d8729 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -297,6 +297,23 @@ let tclIFCATCH a s f =
     | Nil e -> f e
     | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
 
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+    entry-point of [tac] and passes the result of [before] to
+    [finally], which is then run at each exit-point of [tac],
+    regardless of whether it succeeds or fails.  Said another way, if
+    [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+    ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+    [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+    e]. *)
+let rec tclWRAPFINALLY before tac finally =
+  let open Logic_monad in
+  let open Proof in
+  before >>= fun v -> split tac >>= function
+  | Nil e -> finally v >>= fun () -> zero e
+  | Cons (ret,tac') -> plus
+                         (finally v >>= fun () -> return ret)
+                         (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
     with [e], [tclONCE t] also fails with [e]. *)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index d0a2b37a69..70513c8166 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -208,6 +208,16 @@ val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
     exception can be assumed non critical. *)
 val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
 
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+    entry-point of [tac] and passes the result of [before] to
+    [finally], which is then run at each exit-point of [tac],
+    regardless of whether it succeeds or fails.  Said another way, if
+    [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+    ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+    [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+    e]. *)
+val tclWRAPFINALLY : 'a tactic -> 'b tactic -> ('a -> unit tactic) -> 'b tactic
+
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
     with [e], [tclONCE t] also fails with [e]. *)