diff options
| author | Pierre-Marie Pédrot | 2020-11-23 11:19:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-23 11:19:49 +0100 |
| commit | 8b3ad4dc37b55fbf2420b692c352a1c748181411 (patch) | |
| tree | c60d947fcb47c8513e05d2255020b85b12f3a28d /engine/proofview.mli | |
| parent | 0326d06211c49efb4018d65280cf26340f7344b4 (diff) | |
| parent | 6eb6f55499647b9b5a72626839683f6dff9c1549 (diff) | |
Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneously caught
Reviewed-by: ppedrot
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 |