New backtracking system for coq continues, this time it uses a new Coq

command "Bactrack n m p", where n is the global state label to reach
backward, p is the number of aborts and m is an absolute reference to
the proof stack to undo (it is the proof stack depth). Coq prompt is
now like this:

     state                        proof stack
      num                           depth
       __                              _
 aux < 12 |aux|SmallStepAntiReflexive| 4 < ù
 ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^
 usual           pending proofs           usual
                                          special char

See comments in coq-fin-and-forget-v81.

0 files changed, 0 insertions, 0 deletions