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 /proofs/pfedit.mli | |
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 'proofs/pfedit.mli')
-rw-r--r-- | proofs/pfedit.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index b0aacd86c..eca13c56c 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit val undo : int -> unit +(* Same as undo, but undoes the current proof stack to reach depth + [n]. This is used in [vernac_backtrack]. *) +val undo_todepth : int -> unit + +(* Returns the depth of the current focused proof stack, this is used + to put informations in coq prompt (in emacs mode). *) +val current_proof_depth: unit -> int + (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] sets the size to the default value (12) *) |