From 00f333fe7ae2e7bd4ced4be78d24737e62a7b369 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Aug 2015 21:41:17 +0200
Subject: Highlighting of the "Next Obligation" command in CoqIDE.

---
 ide/coq.lang | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/coq.lang b/ide/coq.lang
index 89f93a705e..e25eedbca9 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -122,7 +122,7 @@
         </context>
 
         <context id="proof">
-          <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
+          <start>(Proof(\%{dot_sep}|\%{space}using|\%{space}with))|Next Obligation</start>
           <end>\%{end_proof}\%{dot_sep}</end>
           <include>
             <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-- 
cgit v1.2.3