From 7e60a6ab524a987ee685b4ef76fff1d9bb15c138 Mon Sep 17 00:00:00 2001 From: coq Date: Wed, 20 Apr 2005 16:18:41 +0000 Subject: Implementation of a new backtracking system, that allow to go back anywhere in a script (provided no suspend/resume is used): MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 --- parsing/g_vernacnew.ml4 | 2 ++ 1 file changed, 2 insertions(+) (limited to 'parsing') 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 -- cgit v1.2.3