From f9663fdac4e0204b535abb9a6ff509e5717a82a0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 26 Mar 2015 16:20:30 +0000
Subject: Fixed a smal bug in colorizing response buffer.

First constructor of an inductive was colorized as a hyp name.
Hyp name colorizing should be done another way. Using font-lock here
is probably bad.
---
 coq/coq-syntax.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 0fd200f5..c91ad2d9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1078,7 +1078,7 @@ It is used:
      (cons (proof-regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face)
      (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)
      ;; ", " is for multiple hypothesis diplayed in v8.5.
-     (cons "^ *\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
+     (cons "^  \\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
      (list "^\\([^ \n]+\\) \\(is defined\\)"
            (list 1 'font-lock-function-name-face t)))))
 
-- 
cgit v1.2.3