coq-find-and-forget: re-enable trivial optimisation (is it really

slow in Coq to issue a trivial backtrack to the same spot?)

1 files changed, 0 insertions, 3 deletions

diff --git a/coq/coq.el b/coq/coq.el
index e2e4c4ba..85b28553 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -402,9 +402,6 @@ If locked span already has a state number, then do nothing. Also updates
              (naborts (count-not-intersection 
                        coq-last-but-one-proofstack proofstack)))
     (unless (and 
-             nil
-             ;; FIXME da: these tests go wrong sometimes.
-             ;; Test: Open example.v, C-b, C-r. No backtrack issued.
              ;; 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)