diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 9 |
2 files changed, 14 insertions, 0 deletions
@@ -13,6 +13,11 @@ Tactics - Improved support of dependent goals over objects in dependent types for "destruct". +Vernacular commands + +- New command "Timeout <n> <command>." interprets a command and a timeout + interrupts the interpretation after <n> seconds. + Tools - New coqtop/coqc option -beautify to reformat .v files (usable diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index dfb77e798..52dc36b57 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -852,6 +852,15 @@ go();; This command executes the vernacular command \textrm{\textsl{command}} and display the time needed to execute it. + +\subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout} +\label{time}} + +This command executes the vernacular command \textrm{\textsl{command}}. If +the command has not terminated after the time specified by the integer +(time expressed in seconds), then it is interrupted and an error message +is displayed. + \section{Controlling display} \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent} |