aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b9a104b64..ef6a0b19a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -508,6 +508,14 @@ module New = struct
in
Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if
+ let tclTIMEOUT n t =
+ Proofview.tclOR
+ (Proofview.tclTIMEOUT n t)
+ begin function
+ | Monads.IO.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+ | e -> Proofview.tclZERO e
+ end
+
let nthDecl m =
Proofview.Goal.hyps >>== fun hyps ->
try