diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-04-20 16:18:41 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-04-20 16:18:41 +0000 |
| commit | 7e60a6ab524a987ee685b4ef76fff1d9bb15c138 (patch) | |
| tree | 5e74f1641e0dfa1bd5ad36d417256af3433363ae /parsing | |
| parent | 25b9dd617c7e204f9b93d3cd7dec0d518c90971b (diff) | |
Implementation of a new backtracking system, that allow to go back
anywhere in a script (provided no suspend/resume is used):
* the command "Backtrack n m p" (vernac_bactrack) performs the
following operation:
** do abort p times,
** do undo on the current proof (after the aborts) in order to reach a
stack depth of m (see vernac_undo_todepth)
** resets the global state to state labelled with n.
* The coq prompt in emacs mode has more informations, it contains:
** the usual coq prompt plus:
** the state number (global state label)
** the depth of the current proof stack
** the names of all pending proofs, in *unspecified* order, separated by '|'
Example:
state proof stack
num depth
__ _
aux < 12 |aux|SmallStepAntiReflexive| 4 < รน
^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^
usual pending proofs usual
special char
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index a32e32538..f0350946f 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -647,6 +647,8 @@ GEXTEND Gram | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n + | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> + VernacBacktrack (n,m,p) (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> VernacDebug true |