From 44defeb4542decede229133132539af2e33a6adc Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 11 Sep 2002 14:47:58 +0000
Subject: Check on context menu doesn't seem useful.

---
 coq/coq.el | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 06015bb6..89120a1e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -816,16 +816,22 @@ mouse activation."
 ;; Context-senstive in-span menu additions 
 ;;
 
+;; da: message to Pierre: I just put these in as examples,
+;; maybe you can suggest some better commands to use on
+;; `thm'.  (Check maybe not much use since appears before
+;; in the buffer anyway)
 (defun coq-create-span-menu (span idiom name)
   (if (string-equal idiom "proof")
       (let ((thm (span-property span 'name)))
-        (list (vector
+        (list ;(vector
+              ; "Check"
+              ; `(proof-shell-invisible-command 
+              ;   ,(format "Check %s." thm)))
+              (vector
                "Print Proof"
                `(proof-shell-invisible-command 
                  ,(format "Print Proof %s." thm)))))))
 
-
-
 ;;;   Local Variables: ***
 ;;;   tab-width:2 ***
 ;;;   indent-tabs-mode:nil ***
-- 
cgit v1.2.3