diff options
-rw-r--r-- | pygments/lexers/theorem.py | 10 | ||||
-rw-r--r-- | tests/examplefiles/example_coq.v | 4 |
2 files changed, 9 insertions, 5 deletions
diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py index 293af0ec..98a611ad 100644 --- a/pygments/lexers/theorem.py +++ b/pygments/lexers/theorem.py @@ -41,7 +41,7 @@ class CoqLexer(RegexLexer): 'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save', 'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', - 'outside', + 'outside', 'Check', ) keywords2 = ( # Gallina @@ -62,7 +62,7 @@ class CoqLexer(RegexLexer): 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', - 'split', 'left', 'right', 'autorewrite', + 'split', 'left', 'right', 'autorewrite', 'tauto', ) keywords5 = ( # Terminators @@ -81,9 +81,9 @@ class CoqLexer(RegexLexer): # 'raise', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', # 'type', 'val', 'virtual', 'when', 'while', 'with' keyopts = ( - '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', - r'-\.', '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', - '<-', '=', '>', '>]', '>}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', + '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', + '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', + '<->', '=', '>', '>]', '>}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', r'\[\|', ']', '_', '`', '{', '{<', r'\|', r'\|]', '}', '~', '=>', r'/\\', r'\\/', u'Π', u'λ', diff --git a/tests/examplefiles/example_coq.v b/tests/examplefiles/example_coq.v new file mode 100644 index 00000000..fd1a7bc8 --- /dev/null +++ b/tests/examplefiles/example_coq.v @@ -0,0 +1,4 @@ +Lemma FalseLemma : False <-> False. +tauto. +Qed. +Check FalseLemma. |