diff options
| -rw-r--r-- | ide/highlight.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll index dcb16281b2..d283167c21 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -31,7 +31,7 @@ let ident = firstchar identchar* let keyword = "Add" | "AddPath" | "Chapter" | "CoInductive" | "Compile" | "Defined" | - "End" | "Export" | "Fact" | "Fix" | "Global" | + "End" | "Export" | "Extraction" | "Fact" | "Fix" | "Global" | "Grammar" | "Hint" | "Hints" | ("Hints" space+ "Resolve") | "Immediate" | "Implicits" | "Import" | |