diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
index 487adf3105..176185504f 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),
@@ -154,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
 
 
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