diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-20 16:50:14 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-20 16:50:14 +0000 |
| commit | 3a025b59cb36cad0cd257f31b6e4b8bc22f7060f (patch) | |
| tree | e99fbb4e0049054e78c863a1f0e08f199959fa96 /coq | |
| parent | 7cd8ffc02b605ae4af74570d8c912bae1b1763b3 (diff) | |
removed 'by'form coq-reserved and added it to coq-solve-tactics
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 0ee2e78c..2c8a365b 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -324,6 +324,7 @@ so for the following reasons: coq-user-solve-tactics-db '( ("assumption" "as" "assumption" t "assumption") + ("by" "by" "by #" t "by") ("congruence" "cong" "congruence" t "congruence") ("constructor" "cons" "constructor" t "constructor") ("contradiction" "contr" "contradiction" t "contradiction") @@ -829,7 +830,7 @@ Used by `coq-goal-command-p'" '( "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" "return" "struct" "else" "end" "if" "in" "into" "let" "then" - "using" "with" "by" "beta" "delta" "iota" "zeta" "after" "until" + "using" "with" "beta" "delta" "iota" "zeta" "after" "until" "at" "Sort" "Time" "dest")) "Reserved keywords of Coq.") @@ -946,9 +947,9 @@ Used by `coq-goal-command-p'" (append coq-font-lock-terms (list + (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) |