diff options
| author | Healfdene Goguen | 1997-10-24 14:51:07 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1997-10-24 14:51:07 +0000 |
| commit | 8ef02edc24bd6a65afe23de7f8510b0012f520eb (patch) | |
| tree | bd25fc53aaa3d8f307202318ef7c0e697c453d29 | |
| parent | 05d954c155201ea7b264fc307998f46016168296 (diff) | |
Changed order of "Inversion_clear" and "Inversion" so that former is
fontified first.
Added "Print" to list of commands.
| -rw-r--r-- | coq-fontlock.el | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index 5e9bf556..b3fbfa98 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,11 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.4 1997/10/24 14:51:07 hhg +;; Changed order of "Inversion_clear" and "Inversion" so that former is +;; fontified first. +;; Added "Print" to list of commands. +;; ;; Revision 1.3 1997/10/17 14:45:53 hhg ;; Added "Induction" as tactic ;; @@ -69,12 +74,17 @@ "Hint" "Infix" "Opaque" +"Print" "Pwd" "Reset" "Search" "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" @@ -102,6 +112,7 @@ "Intro" "Intros" "Intuition" +"Inversion_clear" "Inversion" "LApply" "Linear" @@ -113,8 +124,8 @@ "Reflexivity" "Replace" "Rewrite" -"Simpl" "Simplify_eq" +"Simpl" "Specialize" "Symmetry" "Tauto" |