From 3031dc74aa4b42e83dba4e1a97ad4c520731cc14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Apr 2021 20:35:01 +0200
Subject: Fixes #10720: highlighting Variant in CoqIDE.

---
 ide/coqide/coq-ssreflect.lang | 2 +-
 ide/coqide/coq.lang           | 2 +-
 ide/coqide/coq_commands.ml    | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/ide/coqide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang
index fc7bc64a68..d71277f42c 100644
--- a/ide/coqide/coq-ssreflect.lang
+++ b/ide/coqide/coq-ssreflect.lang
@@ -32,7 +32,7 @@
     <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex>
     <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
+    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Variant)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
     <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
     <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
     <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
diff --git a/ide/coqide/coq.lang b/ide/coqide/coq.lang
index e9eab48de7..e6e813aca2 100644
--- a/ide/coqide/coq.lang
+++ b/ide/coqide/coq.lang
@@ -29,7 +29,7 @@
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
     <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
-    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Variant|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
     <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 2d75ad9ff6..6e02d7fed1 100644
--- a/ide/coqide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
@@ -151,6 +151,7 @@ let commands = [
    "Unset Silent.";
    "Unset Undo";];
   ["Variable";
+   "Variant";
    "Variables";];
   ["Write State";];
 ]
-- 
cgit v1.2.3