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.

1 files changed, 7 insertions, 4 deletions

diff --git a/lib/control.mli b/lib/control.mli
index 25135934bc..9465d8f0d5 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -10,6 +10,9 @@
 
 (** Global control of Coq. *)
 
+(** Used to convert signals to exceptions *)
+exception Timeout
+
 (** Will periodically call [Thread.delay] if set to true *)
 val enable_thread_delay : bool ref
 
@@ -21,13 +24,13 @@ val check_for_interrupt : unit -> unit
 (** Use this function as a potential yield function. If {!interrupt} has been
     set, il will raise [Sys.Break]. *)
 
-val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b
-(** [timeout n f x e] tries to compute [f x], and if it fails to do so
-    before [n] seconds, it raises [e] instead. *)
+val timeout : int -> ('a -> 'b) -> 'a -> 'b option
+(** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so
+    before [n] seconds, returns [None] instead. *)
 
 (** Set a particular timeout function; warning, this is an internal
    API and it is scheduled to go away. *)
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
 val set_timeout : timeout -> unit
 
 (** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that