diff options
| author | Kazuhiko Sakaguchi <pi8027@gmail.com> | 2021-12-10 23:42:39 +0900 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-10 15:42:39 +0100 |
| commit | 22131277ce57ebaeebf4a102b811aad6d4cacecc (patch) | |
| tree | 3c1b8164f17e62310663daac4ca30069784b6f26 /pygments/lexers/theorem.py | |
| parent | 4f228fa5dba43e0e4ef3b706f415e9a5fef1852a (diff) | |
| download | pygments-git-22131277ce57ebaeebf4a102b811aad6d4cacecc.tar.gz | |
Add missing keywords (Vernacular commands and tactics) for the Coq lexer (#1984)
Diffstat (limited to 'pygments/lexers/theorem.py')
| -rw-r--r-- | pygments/lexers/theorem.py | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py index ec55a32e..a7f4330a 100644 --- a/pygments/lexers/theorem.py +++ b/pygments/lexers/theorem.py @@ -34,16 +34,16 @@ class CoqLexer(RegexLexer): keywords1 = ( # Vernacular commands 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable', - 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Hypothesis', + 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Axioms', 'Hypothesis', 'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope', - 'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Let', 'Ltac', - 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', - 'Arguments', 'Set', 'Unset', 'Contextual', 'Strict', 'Prenex', + 'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Example', 'Let', + 'Ltac', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', + 'Arguments', 'Types', 'Set', 'Unset', 'Contextual', 'Strict', 'Prenex', 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', - 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Corollary', - 'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save', - 'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', - 'Abort', 'Admitted', + 'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact', + 'Remark', 'Corollary', 'Proposition', 'Property', 'Goal', + 'Proof', 'Restart', 'Save', 'Qed', 'Defined', 'Abort', 'Admitted', + 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', 'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing', 'Universe', 'Polymorphic', 'Monomorphic', 'Context' @@ -74,7 +74,8 @@ class CoqLexer(RegexLexer): ) keywords5 = ( # Terminators - 'by', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega', + 'by', 'now', 'done', 'exact', 'reflexivity', + 'tauto', 'romega', 'omega', 'lia', 'nia', 'lra', 'nra', 'psatz', 'assumption', 'solve', 'contradiction', 'discriminate', 'congruence', ) |