diff options
| author | barras | 2009-03-04 19:35:34 +0000 |
|---|---|---|
| committer | barras | 2009-03-04 19:35:34 +0000 |
| commit | 93b16c35bb0177847d91f26d2d8ad45f20fe4b5c (patch) | |
| tree | 99967d0c7dcf3224600cfe2a05f69c1e51424997 | |
| parent | 75345335b8d6a3c1539f9e05f7a7c587d920410e (diff) | |
doc et CHANGES pour la commande Timeout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11962 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 dfb77e7987..52dc36b575 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} |