diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-06-03 18:01:54 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1998-06-03 18:01:54 +0000 |
| commit | cc0f80562346189d6bf8e98590f09474f74ba31e (patch) | |
| tree | 7c07cbfb34cee5227a7687fa1f82f44985f1d12e /coq-fontlock.el | |
| parent | 4257ca2e973a34c4bdb6ab6f9d7371b4dcabe779 (diff) | |
Changed Compute from command to tactic.
Added Fix, Destruct and Cofix as tactics.
Added Local as goal.
Diffstat (limited to 'coq-fontlock.el')
| -rw-r--r-- | coq-fontlock.el | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index eea19e25..0a2dddf9 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,11 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.12 1998/06/03 18:01:54 hhg +;; Changed Compute from command to tactic. +;; Added Fix, Destruct and Cofix as tactics. +;; Added Local as goal. +;; ;; Revision 1.11 1998/06/02 15:33:16 hhg ;; Minor modifications to comments ;; @@ -77,6 +82,7 @@ "Fact" "Goal" "Lemma" +"Local" "Remark" "Theorem" )) @@ -98,7 +104,6 @@ "Cd" "Check" "Class" -"Compute" "Coercion" "DelPath" "Eval" @@ -126,12 +131,15 @@ "Case" "Change" "Clear" +"Cofix" +"Compute" "Constructor" "Contradiction" "Cut" "DHyp" "DInd" "Dependent" +"Destruct" "Discriminate" "Double" "EApply" @@ -140,6 +148,7 @@ "End" "Exact" "Exists" +"Fix" "Generalize" "Grammar" "Hnf" |