| 1 | | Actually, I misspoke. The problem is that ProofGeneral is using a deprecated command: `Backtrack` instead of `BackTo`. By using `BackTo`, things work again as expected: |
| 2 | | |
| 3 | | {{{ |
| 4 | | (defun coq-find-and-forget (span) |
| 5 | | "Backtrack to SPAN. Using the \"BackTo n\" coq command." |
| 6 | | (if (eq (span-property span 'type) 'proverproc) |
| 7 | | ;; processed externally (i.e. Require, etc), nothing to do |
| 8 | | ;; (should really be unlocked when we undo the Require). |
| 9 | | nil |
| 10 | | (let* (ans (nundos 0) |
| 11 | | (proofdepth (coq-get-span-proofnum span)) |
| 12 | | (proofstack (coq-get-span-proofstack span)) |
| 13 | | (span-staten (coq-get-span-statenum span))) |
| 14 | | ;; if we move outside of any proof, coq does not print anything, so clean |
| 15 | | ;; the goals buffer otherwise the old one will still be displayed |
| 16 | | (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer)) |
| 17 | | (unless (and |
| 18 | | ;; return nil (was proof-no-command) in this case: |
| 19 | | ;; this is more efficient as backtrack x y z may be slow |
| 20 | | (equal coq-last-but-one-proofstack proofstack) |
| 21 | | (= coq-last-but-one-proofnum proofdepth) |
| 22 | | (= coq-last-but-one-statenum span-staten)) |
| 23 | | (list |
| 24 | | (format "BackTo %s . " |
| 25 | | (int-to-string span-staten))))))) |
| 26 | | }}} |
| | 1 | It happens in Coq with BackTo as well. |
