summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pygments/lexers/theorem.py10
-rw-r--r--tests/examplefiles/example_coq.v4
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.