Move tclWRAPFINALLY to profile_ltac

As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef

3 files changed, 19 insertions, 29 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 1d2c7d8729..2e036be9e3 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -297,23 +297,6 @@ 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 70513c8166..d0a2b37a69 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -208,16 +208,6 @@ 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]. *)
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 44cb531e51..0dbf16a821 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -330,15 +330,32 @@ let exit_tactic ~count_call start_time c =
       feedback_results parent
     end
 
+(** [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 Proofview in
+  let open Proofview.Notations in
+  before >>= fun v -> tclCASE tac >>= function
+  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Next (ret, tac') -> tclOR
+                          (finally v >>= fun () -> tclUNIT ret)
+                          (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
 let do_profile s call_trace ?(count_call=true) tac =
   let open Proofview.Notations in
   (* We do an early check to [is_profiling] so that we save the
-     overhead of [Proofview.tclWRAPFINALLY] when profiling is not set
+     overhead of [tclWRAPFINALLY] when profiling is not set
      *)
   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
   | false -> tac
   | true ->
-    Proofview.tclWRAPFINALLY
+    tclWRAPFINALLY
       (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
            if !is_profiling then
              match call_trace, Local.(!stack) with