diff options
| author | Emilio Jesus Gallego Arias | 2019-08-01 15:14:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-27 16:57:23 +0200 |
| commit | 94c8f42eea1c36f582fe2390680de75634324c85 (patch) | |
| tree | 56cf6addaf2c97d26855437cc78a3becf1ef726d /engine/logic_monad.ml | |
| parent | 1e1d5bf3879424688fa9231ba057b05d86674d22 (diff) | |
[cleanup] Replace uses of UserError constructor, clarify exception names.
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
Diffstat (limited to 'engine/logic_monad.ml')
| -rw-r--r-- | engine/logic_monad.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 7c06bb59f1..e3a5676942 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system @@ -38,7 +38,6 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> raise CErrors.Unhandled @@ -99,7 +98,7 @@ struct let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t () (Exception Timeout) + Control.timeout n t () (Exception Tac_Timeout) let make f = (); fun () -> try f () |