From cb48d3cf0936a350fe0d1b7527f08440c18258be Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 31 Aug 2002 13:04:10 +0000
Subject: Improved implementation of zap-commas font lock behaviour, patch from
 Stefan Monnier

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

(limited to 'coq')

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index dce173e2..e8f1fe64 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -455,7 +455,9 @@ Idtac (Nop) tactic, put the following line in your .emacs:
      (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
-     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
+     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
+     ;; Remove spurious variable and function faces on commas.
+     '(proof-zap-commas))))
 (defvar coq-font-lock-keywords coq-font-lock-keywords-1)
 
 (defun coq-init-syntax-table ()
diff --git a/coq/coq.el b/coq/coq.el
index 641fc1b4..06015bb6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -680,8 +680,6 @@ This is specific to coq-mode."
 
   (setq font-lock-keywords coq-font-lock-keywords-1)
 
-  (setq proof-font-lock-zap-commas t)	; enable the painful hack
-  
   (proof-config-done)
 
 ;; outline
-- 
cgit v1.2.3