diff options
| author | Lasse Blaauwbroek | 2020-11-14 12:35:21 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-11-22 11:18:52 +0100 |
| commit | 6eb6f55499647b9b5a72626839683f6dff9c1549 (patch) | |
| tree | f19236e8f9ee6be3f6e09ed354911b4b4ddd7d07 /engine/proofview.mli | |
| parent | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff) | |
Fix timeout by ensuring signal exceptions are not erroneously caught
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 816b45984b..fe0d7ae51e 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -417,7 +417,7 @@ end val tclCHECKINTERRUPT : unit tactic (** [tclTIMEOUT n t] can have only one success. - In case of timeout if fails with [tclZERO Timeout]. *) + In case of timeout it fails with [tclZERO Tac_Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic (** [tclTIME s t] displays time for each atomic call to t, using s as an |