From 8426dacbd89350acca31c8552df80f3bcf68252e Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Thu, 6 Nov 1997 16:46:20 +0000
Subject: Updates to Coq fontlock tables

---
 coq-fontlock.el | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/coq-fontlock.el b/coq-fontlock.el
index 8f2672c0..166eb66d 100644
--- a/coq-fontlock.el
+++ b/coq-fontlock.el
@@ -4,6 +4,9 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.6  1997/11/06 16:46:20  hhg
+;; Updates to Coq fontlock tables
+;;
 ;; Revision 1.5  1997/10/30 15:58:29  hhg
 ;; Updates for coq, including:
 ;; 	* pbp-goal-command and pbp-hyp-command use proof-terminal-string
@@ -44,6 +47,7 @@
 (defvar coq-keywords-defn
   '(
 "Definition"
+"Fixpoint"
 "Inductive"
 ))
 
@@ -84,13 +88,10 @@
 "Pwd"
 "Reset"
 "Search"
+"Show"
 "Transparent"
 ))
 
-; There seems to be a bug with fontlock: "_" is part of the symbol
-; table, but fontlock doesn't fontify "Inversion_clear" but only
-; "Inversion" -- hhg
-
 (defvar coq-tactics
   '(
 "Absurd"
@@ -99,6 +100,7 @@
 "Auto"
 "Case"
 "Change"
+"Clear"
 "Constructor"
 "Contradiction"
 "Cut"
-- 
cgit v1.2.3