From 84357f0d15a1137a4b1cc5cacb86d3af5c1ca93e Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 2 Nov 2013 15:34:12 +0000
Subject: Bases tactics on an IO monad.

It allowed to restore the timeout tactics. It also prepares for the debugging
mechanism to be restored.

['a IO.t] is just [unit -> 'a].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacticals.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tactics/tacticals.ml')

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
-- 
cgit v1.2.3