diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-18 11:03:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-18 11:03:03 +0000 |
| commit | 404c0f9c6b189c4273a9bc1698765eaa6a664389 (patch) | |
| tree | b4465ccce38000ffb63487e86e709bd15fe54d90 /parsing/g_ltac.ml4 | |
| parent | a2f26ddde0c5ee088a4a65ab9708085c16a8ba48 (diff) | |
A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds
Note: even if this new tactical can be quite handy during the development phase,
(for instance to bound the time allocated to some search tactics), please be aware
of its main drawback: with it, scripts are no longer machine-independant, something
that works on a quick machine may fail on a slow one. The converse is even possible
if you combine this "timeout" with other tactic combinators. We strongly advise to
not leave any "timeout" in the final version of a development.
In addition, this feature won't probably work on native win32, since Unix.alarm
isn't implemented.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1d100c7cc..e71d53bf9 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -57,6 +57,7 @@ GEXTEND Gram | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta (*To do: put Abstract in Refiner*) |