diff options
| author | Emilio Jesus Gallego Arias | 2020-01-30 23:00:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-24 12:41:28 -0500 |
| commit | 5f5b8a1fdfc71ae93f75d5bfa2d6bb2920a2f4d1 (patch) | |
| tree | c2236854ca6d3de29cbe5e6d42e11766c4115ddb /engine | |
| parent | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (diff) | |
[exn] remove `raise` taking optional exception information argument
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/logic_monad.ml | 5 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 3c383b2e00..6df3378524 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -83,7 +83,7 @@ struct (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) + let raise (e, info) () = Exninfo.iraise (Exception e, info) (** [try ... with ...] but restricted to {!Exception}. *) let catch = fun s h -> (); @@ -93,7 +93,8 @@ struct h (e, info) () let read_line = fun () -> try read_line () with e -> - let (e, info) = CErrors.push e in raise ~info e () + let (e, info) = CErrors.push e in + raise (e, info) () let print_char = fun c -> (); fun () -> print_char c diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 75920455ce..5002d24af0 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -70,7 +70,7 @@ module NonLogical : sig (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - val raise : ?info:Exninfo.info -> exn -> 'a t + val raise : Exninfo.iexn -> 'a t (** [try ... with ...] but restricted to {!Exception}. *) val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t diff --git a/engine/proofview.ml b/engine/proofview.ml index b0ea75ac60..690b1620b9 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -937,7 +937,7 @@ let tclTIMEOUT n t = return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) - | e -> Logic_monad.NonLogical.raise ~info e + | e -> Logic_monad.NonLogical.raise (e, info) end end >>= function | Util.Inl (res,s,m,i) -> |