Fixed disabled proof using menu.

1 files changed, 1 insertions, 1 deletions

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'." )