Changes between Initial Version and Version 1 of Ticket #495, comment 2


Ignore:
Timestamp:
Sep 6, 2014, 8:52:37 AM (10 years ago)
Author:
coquser
Comment:

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #495, comment 2

    initial v1  
    33{{{
    44(defun coq-find-and-forget (span)
    5   "Backtrack to SPAN.  Using the \"BackTo n m p\" coq command."
     5  "Backtrack to SPAN.  Using the \"BackTo n\" coq command."
    66  (if (eq (span-property span 'type) 'proverproc)
    77      ;; processed externally (i.e. Require, etc), nothing to do
    88      ;; (should really be unlocked when we undo the Require).
    99      nil
    10   (let* (ans (naborts 0) (nundos 0)
     10  (let* (ans (nundos 0)
    1111             (proofdepth (coq-get-span-proofnum span))
    1212             (proofstack (coq-get-span-proofstack span))
    13              (span-staten (coq-get-span-statenum span))
    14              (naborts (count-not-intersection
    15                        coq-last-but-one-proofstack proofstack)))
     13             (span-staten (coq-get-span-statenum span)))
    1614    ;; if we move outside of any proof, coq does not print anything, so clean
    1715    ;; the goals buffer otherwise the old one will still be displayed