From 59190289edf805e3de3e6025f57295a287a0cf9d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 15 Apr 2020 18:13:13 +0200
Subject: Fixed disabled proof using menu.

---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index 8e9ee9d1..5dc45a9a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2618,7 +2618,7 @@ Remarks and limitations:
            (fn `(lambda (sp)
                  (coq-insert-proof-using-suggestion sp t)
                  (span-delete ,specialspan))))
-      (list "-------------" (vector name `(,fn ,span) (not (not deps))))))
+      (list "-------------" (vector name `(,fn ,span) t))))
   "Coq specific additional menu entry for \"Proof using\".
 annotation. See `proof-dependency-menu-system-specific'." )
 
-- 
cgit v1.2.3