Documentation of the timeout tactical (cf r13917)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 090bbb0a92..793c364dea 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -100,6 +100,7 @@ is understood as
 & | & {\tt progress} {\tacexprpref}\\
 & | & {\tt repeat} {\tacexprpref}\\
 & | & {\tt try} {\tacexprpref}\\
+& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -443,6 +444,28 @@ This is a combination of the previous variants.
 
 \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
 
+\subsubsection[Timeout]{Timeout\tacindex{timeout}
+\index{Tacticals!timeout@{\tt timeout}}}
+
+We can force a tactic to stop if it has not finished after a certain
+amount of time:
+\begin{quote}
+{\tt timeout} {\num} {\tacexpr}
+\end{quote}
+{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+normally applied, except that it is interrupted after ${\num}$ seconds
+if it is still running. In this case the outcome is a failure.
+
+Warning: For the moment, {\tt timeout} is based on elapsed time in
+seconds, which is very
+machine-dependent: a script that works on a quick machine may fail
+on a slow one. The converse is even possible if you combine a
+{\tt timeout} with some other tacticals. This tactical is hence
+proposed only for convenience during debug or other development
+phases, we strongly advise you to not leave any {\tt timeout} in
+final scripts. Note also that this tactical isn't available on
+the native Windows port of Coq.
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let}
 \index{Ltac!let rec}
 \index{let!in Ltac}