Move tclWRAPFINALLY to profile_ltac

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

2 files changed, 0 insertions, 27 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]. *)