From d8dcc5a9a4e4c8bf55b697f8a9a1f85fe1240356 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 25 Aug 2010 09:38:02 +0000
Subject: coq-find-and-forget: re-enable trivial optimisation (is it really
 slow in Coq to issue a trivial backtrack to the same spot?)

---
 coq/coq.el | 3 ---
 1 file changed, 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)
-- 
cgit v1.2.3