diff options
| author | aspiwack | 2013-11-02 15:34:12 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:34:12 +0000 |
| commit | 84357f0d15a1137a4b1cc5cacb86d3af5c1ca93e (patch) | |
| tree | 9d6b50c88ca6550048318ac19f74522d76b45f69 /tactics | |
| parent | 1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
3 files changed, 11 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 45ece0ba4a..d788ade4d0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1118,7 +1118,7 @@ and eval_tactic ist = function (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac) - | TacTimeout (n,tac) -> Proofview.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b9a104b64a..ef6a0b19a0 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 diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index d32a0dab7b..d0dae09932 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,6 +223,8 @@ module New : sig val tclSOLVE : unit tactic list -> unit tactic val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic + val tclTIMEOUT : int -> unit tactic -> unit tactic + val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> |