From 6acfaf0683cc83e1ff047d1a834ebb707c1e3269 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 22 Feb 1999 14:54:02 +0000
Subject: Comments from Healf explaining need for coq-goal-command-p

---
 coq/coq-syntax.el | 5 -----
 coq/coq.el        | 7 +++++--
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a696cf32..16f2a15f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -28,11 +28,6 @@
 "Scheme"
 ))
 
-;; FIXME da: I'm not sure why this variable includes more than
-;; just the Goal-type commands.  Perhaps it was so that func-menu
-;; worked neatly, but it leads to the nasty use of proof-goal-command-p
-;; instead of a proof-goal-regexp.  Func menu configuration has since
-;; been overhauled, so this could maybe be improved now.
 (defvar coq-keywords-goal
   '(
 "Definition"
diff --git a/coq/coq.el b/coq/coq.el
index 160ec044..cfca4ec0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -145,8 +145,11 @@
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
   "Declaration and definition regexp.")
 
-;; FIXME da: this one function breaks the nice configuration of Proof General:
-;; should have proof-goal-regexp instead.
+;; da: this one function breaks the nice configuration of Proof General:
+;; would be nice to have proof-goal-regexp instead.
+;; Unfortunately Coq allows Goals beginning with "Definition" and the 
+;; like, so it is difficult to have just a proof-goal-regexp setting.  
+
 (defun coq-goal-command-p (str)
   "Decide whether argument is a goal or not"
   (and (proof-string-match coq-goal-command-regexp str)
-- 
cgit v1.2.3