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

0 files changed, 0 insertions, 0 deletions