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

1 files changed, 2 insertions, 0 deletions

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 1adc2aeb18..6bea86fec4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -475,6 +475,8 @@ let rec pr_vernac = function
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
   | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacBacktrack (i,j,k) -> 
+      str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
   | VernacFocus i -> str"Focus" ++ pr_opt int i
   | VernacGo g -> 
       let pr_goable = function