Goals buffer aggressively cleared with Coq pre-8.5

[coquser]

I am using Proof General 4.3pre131011 with the current trunk version of Coq (pre-8.5).

With 8.4pl4, if I type period to end a tactic, my goals buffer update. If I delete the period, the goals buffer changes to what it had displayed immediately before. This is the desired behavior.

With 8.5pre, when I delete the period it clears the goals buffer, and does not display again until I press the period, making it extremely difficult to replay what changes a certain tactic made to my environment.

[coquser]

I've tracked down what is going on, and it looks like a Coq issue: Calls to Backtrack are not reprinting the goal. I will pursue this bug on the Coq bug tracker.

[coquser]

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:

(defun coq-find-and-forget (span)
  "Backtrack to SPAN.  Using the \"BackTo n\" coq command."
  (if (eq (span-property span 'type) 'proverproc)
      ;; processed externally (i.e. Require, etc), nothing to do
      ;; (should really be unlocked when we undo the Require).
      nil
  (let* (ans (nundos 0)
             (proofdepth (coq-get-span-proofnum span))
             (proofstack (coq-get-span-proofstack span))
             (span-staten (coq-get-span-statenum span)))
    ;; if we move outside of any proof, coq does not print anything, so clean
    ;; the goals buffer otherwise the old one will still be displayed
    (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer))
    (unless (and
             ;; return nil (was proof-no-command) in this case:
             ;; this is more efficient as backtrack x y z may be slow
             (equal coq-last-but-one-proofstack proofstack)
             (= coq-last-but-one-proofnum proofdepth)
             (= coq-last-but-one-statenum span-staten))
      (list
       (format "BackTo %s . "
               (int-to-string span-staten)))))))