1 files changed, 28 insertions, 6 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d8747254..38ad9aa8 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} & ::= &
@@ -446,6 +447,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}
@@ -568,11 +591,10 @@ pattern:
 \begin{quote}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
 \end{quote}
-It matches any term which one subterm matches {\cpattern}. If there is
-a match, the optional {\ident} is assign the ``matched context'', that
-is the initial term where the matched subterm is replaced by a
-hole. The definition of {\tt context} in expressions below will show
-how to use such term contexts.
+It matches any term with a subterm matching {\cpattern}. If there is
+a match, the optional {\ident} is assigned the ``matched context'', i.e.
+the initial term where the matched subterm is replaced by a
+hole. The example below will show how to use such term contexts.
 
 If the evaluation of the right-hand-side of a valid match fails, the
 next matching subterm is tried. If no further subterm matches, the
@@ -606,7 +628,7 @@ Alternatively, one may now use the following variant of {\tt context}:
 The behavior of {\tt appcontext} is the same as the one of {\tt
   context}, except that a matching subterm could be a partial
 part of a longer application. For instance, in {\tt (f 1 2)},
-an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}.
+an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. 
 
 \end{Variants}