From 1fe8a6717a51a616f97a3d5f130003301d64e963 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 6 Mar 2015 16:57:20 +0100
Subject: Fix syntax highlighting of Extraction Inline and add Separate
Extraction.
---
ide/coq.lang | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/ide/coq.lang b/ide/coq.lang
index fee84bd32e..e13a94aeac 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -197,7 +197,6 @@
Arguments
Implicit\%{space}+Arguments
Include
- (Recursive\%{space}+)?Extraction(\%{space}+((Library)|((No)?Inline)|(Blacklist)))?
Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive))
@@ -210,6 +209,7 @@
Require(\%{space}+((Import)|(Export)))?
Import
Export
+ ((Recursive|Separate)\%{space}+)?Extraction(\%{space}+(Library|(No)?Inline|Blacklist))?
--
cgit v1.2.3