[exninfo] Deprecate aliases for exception re-raising.

We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.

At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.

1 files changed, 8 insertions, 9 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index a92179ab5b..5bfbc6a649 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -14,7 +14,6 @@
     ['a tactic] is the (abstract) type of tactics modifying the proof
     state and returning a value of type ['a]. *)
 
-open Util
 open EConstr
 
 (** Main state of tactics *)
@@ -194,18 +193,18 @@ val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
     the successes of [t1] have been depleted and it failed with [e],
     then it behaves as [t2 e]. In other words, [tclOR] inserts a
     backtracking point. *)
-val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
+val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
 
 (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
     success or [t2 e] if [t1] fails with [e]. It is analogous to
     [try/with] handler of exception in that it is not a backtracking
     point. *)
-val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
+val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
 
 (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
     succeeds at least once then it behaves as [tclBIND a s] otherwise,
     if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
+val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b 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
@@ -227,8 +226,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
     continuation. It is the most general primitive to control
     backtracking. *)
 type 'a case =
-  | Fail of iexn
-  | Next of 'a * (iexn -> 'a tactic)
+  | Fail of Exninfo.iexn
+  | Next of 'a * (Exninfo.iexn -> 'a tactic)
 val tclCASE : 'a tactic -> 'a case tactic
 
 (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
@@ -236,7 +235,7 @@ val tclCASE : 'a tactic -> 'a case tactic
     failure with an exception [e] such that [p e = Some e'] is raised. At
     which point it drops the remaining successes, failing with [e'].
     [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
+val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic
 
 
 (** {7 Focusing tactics} *)
@@ -508,8 +507,8 @@ end
 module UnsafeRepr :
 sig
   type state = Proofview_monad.Logical.Unsafe.state
-  val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
-  val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
+  val repr : 'a tactic -> ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t
+  val make : ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t -> 'a tactic
 end
 
 (** {6 Goal-dependent tactics} *)