diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-29 08:23:49 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-29 08:23:49 +0000 |
| commit | 06b70d642a2f2ff48eddf78298eeb2cf71f4f4eb (patch) | |
| tree | 25df6c9c1a6ca64849c69ac3135328d9ee020831 /coq | |
| parent | 8b9d015e41d5c7a1498eb91141496fdb5eb27c2d (diff) | |
V8/V7 reserved keywords for coq
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 34 |
1 files changed, 25 insertions, 9 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 80e0cdb1..eb1f2d3d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -679,30 +679,46 @@ Idtac (Nop) tactic, put the following line in your .emacs: "Try") "Keywords for tacticals in a Coq script.") -(defvar coq-reserved +; From JF Monin: +(defvar coq-reserved-common '("as" - "ALL" "True" "False" - "Cases" - "match" - "EX" "else" "end" - "Fix" - "forall" - "fun" "if" "in" "into" "let" - "of" "then" "using" "with" "after") "Reserved keywords of Coq.") +(defvar coq-reserved-V8 + '( + "cofix" + "fix" + "struct" + "match" + "forall" + "fun" + )) + +(defvar coq-reserved-V7 + '( + "ALL" "Cases" "EX" "Fix" "of" "CoFix" + )) + +(defvar coq-reserved + (cond + (coq-version-is-V8 + (append coq-reserved-common coq-reserved-V8)) + (t + (append coq-reserved-common coq-reserved-V7)))) + + (defvar coq-symbols '("|" ":" |