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 /lib/heap.ml | |
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 'lib/heap.ml')
0 files changed, 0 insertions, 0 deletions