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, 6 insertions, 16 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 978088872c..22863f451d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -937,22 +937,12 @@ let tclTIMEOUT n t =
   Proof.get >>= fun initial ->
   Proof.current >>= fun envvar ->
   Proof.lift begin
-    Logic_monad.NonLogical.catch
-      begin
-        let open Logic_monad.NonLogical in
-        timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
-        match r with
-        | Logic_monad.Nil e -> return (Util.Inr e)
-        | Logic_monad.Cons (r, _) -> return (Util.Inl r)
-      end
-      begin let open Logic_monad.NonLogical in function (e, info) ->
-        match e with
-        | Logic_monad.Tac_Timeout ->
-          return (Util.Inr (Logic_monad.Tac_Timeout, info))
-        | Logic_monad.TacticFailure e ->
-          return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise (e, info)
-      end
+    let open Logic_monad.NonLogical in
+    timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
+    match r with
+    | None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null))
+    | Some (Logic_monad.Nil e) -> return (Util.Inr e)
+    | Some (Logic_monad.Cons (r, _)) -> return (Util.Inl r)
   end >>= function
     | Util.Inl (res,s,m,i) ->
         Proof.set s >>