From a1e8e27840d6d30091dae9c8555ff1bc9ee4aa1f Mon Sep 17 00:00:00 2001
From: Maximilian Wuttke <mwuttke97@posteo.de>
Date: Fri, 25 Dec 2020 21:04:26 +0100
Subject: [PATCH 1/3] Unicode support for Coq

Catch-all lexing for `Name.Builtin.Pseudo`, as in the lean lexer.

This fixes #678.
---
 pygments/lexers/theorem.py | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
index 487adf3105..82739dd1b0 100644
--- a/pygments/lexers/theorem.py
+++ b/pygments/lexers/theorem.py
@@ -30,6 +30,8 @@ class CoqLexer(RegexLexer):
     filenames = ['*.v']
     mimetypes = ['text/x-coq']
 
+    flags = re.UNICODE
+
     keywords1 = (
         # Vernacular commands
         'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable',
@@ -123,14 +125,15 @@ class CoqLexer(RegexLexer):
             (r'0[bB][01][01_]*', Number.Bin),
             (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
 
-            (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'",
-             String.Char),
+            (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", String.Char),
+
             (r"'.'", String.Char),
             (r"'", Keyword),  # a stray quote is another syntax element
 
             (r'"', String.Double, 'string'),
 
             (r'[~?][a-z][\w\']*:', Name),
+            (r'\S', Name.Builtin.Pseudo),
         ],
         'comment': [
             (r'[^(*)]+', Comment),

From 2ce788d59dac9b9e072d5e66a5fbe0352217b133 Mon Sep 17 00:00:00 2001
From: Maximilian Wuttke <mwuttke97@posteo.de>
Date: Fri, 25 Dec 2020 21:06:18 +0100
Subject: [PATCH 2/3] Coq lexer: improve `analyse_text`

---
 pygments/lexers/theorem.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
index 82739dd1b0..176185504f 100644
--- a/pygments/lexers/theorem.py
+++ b/pygments/lexers/theorem.py
@@ -157,7 +157,7 @@ class CoqLexer(RegexLexer):
     }
 
     def analyse_text(text):
-        if 'qed' in text and 'tauto' in text:
+        if 'Qed' in text and 'Proof' in text:
             return 1
 
 

From 02cd333e8b5d83eddf177e306ea5fb9d25f6b2ee Mon Sep 17 00:00:00 2001
From: Maximilian Wuttke <mwuttke97@posteo.de>
Date: Mon, 28 Dec 2020 17:56:02 +0100
Subject: [PATCH 3/3] Add a test for Coq

---
 tests/test_coq.py | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 tests/test_coq.py

diff --git a/tests/test_coq.py b/tests/test_coq.py
new file mode 100644
index 0000000000..6b4e27da06
--- /dev/null
+++ b/tests/test_coq.py
@@ -0,0 +1,33 @@
+# -*- coding: utf-8 -*-
+"""
+    Coq Tests
+    ~~~~~~~~~~~~~
+    :copyright: Copyright 2006-2020 by the Pygments team, see AUTHORS.
+    :license: BSD, see LICENSE for details.
+"""
+
+import pytest
+
+from pygments.lexers import CoqLexer
+from pygments.token import Token
+
+@pytest.fixture(scope='module')
+def lexer():
+    yield CoqLexer()
+
+def test_coq_unicode(lexer):
+    fragment = 'Check (α ≻ β).\n'
+    tokens = [
+        (Token.Keyword.Namespace, 'Check'),
+        (Token.Text, ' '),
+        (Token.Operator, '('),
+        (Token.Name, 'α'),
+        (Token.Text, ' '),
+        (Token.Name.Builtin.Pseudo, '≻'),
+        (Token.Text, ' '),
+        (Token.Name, 'β'),
+        (Token.Operator, ')'),
+        (Token.Operator, '.'),
+        (Token.Text, '\n'),
+    ]
+    assert list(lexer.get_tokens(fragment)) == tokens