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 /tactics/tacticals.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 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2d0806b2e0..b93c4a176f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -546,7 +546,8 @@ module New = struct Proofview.tclOR (Proofview.tclTIMEOUT n t) begin function (e, info) -> match e with - | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) + | Logic_monad.Tac_Timeout as e -> + Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) | e -> Proofview.tclZERO ~info e end |