From 591e7e484d544e958595a0fb784336ae050a9c74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:47 +0200 Subject: Highlighting Universe in CoqIDE. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/coq.lang b/ide/coq.lang index c65432bdb7..89f93a705e 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,7 +29,7 @@ (\%{ident}\.)*\%{ident} \.(\s|\z) ([-+*]+|{)(\s|\z)|}(\s*})* - Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion + Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)? ((Local|Global)\%{space})? Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property -- cgit v1.2.3