diff options
| author | Healfdene Goguen | 1997-11-06 16:46:20 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1997-11-06 16:46:20 +0000 |
| commit | 8426dacbd89350acca31c8552df80f3bcf68252e (patch) | |
| tree | 6e87ea22037b4ccc50a64a2d992d1ed460c69d43 | |
| parent | 22720e8ed76564289f6e1c35ad1ce2fc1794fadb (diff) | |
Updates to Coq fontlock tables
| -rw-r--r-- | coq-fontlock.el | 10 |
1 files 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" |