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, 1 insertions, 1 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 982814fdfc..095ee61835 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1943,7 +1943,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
               try (* First try finding a subterm w/o conversion on open terms *)
                 let flags = set_no_delta_open_flags flags in
                 w_unify_to_subterm env evd ~flags t'
-              with e ->
+              with e when CErrors.noncritical e ->
                 (* If this fails, try with full conversion *)
                 w_unify_to_subterm env evd ~flags t'
             else w_unify_to_subterm env evd ~flags t'