summaryrefslogtreecommitdiff
path: root/ide/highlight.mll
diff options
context:
space:
mode:
Diffstat (limited to 'ide/highlight.mll')
-rw-r--r--ide/highlight.mll9
1 files changed, 6 insertions, 3 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 21063459..e2a1d0cd 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: highlight.mll,v 1.14.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: highlight.mll,v 1.14.2.2 2004/11/27 14:41:43 herbelin Exp $ *)
{
@@ -29,18 +29,21 @@ let identchar =
let ident = firstchar identchar*
let keyword =
- "Add" | "CoInductive" | "Defined" |
+ "Add" | "Defined" |
"End" | "Export" | "Extraction" | "Hint" |
"Implicits" | "Import" |
"Infix" | "Load" | "match" | "Module" | "Module Type" |
"Proof" | "Qed" |
- "Record" | "Require" | "Save" | "Scheme" |
+ "Require" | "Save" | "Scheme" |
"Section" | "Unset" |
"Set"
let declaration =
"Lemma" | "Axiom" | "CoFixpoint" | "Definition" |
"Fixpoint" | "Hypothesis" |
+ "Hypotheses" | "Axioms" | "Parameters" | "Subclass" |
+ "Remark" | "Fact" | "Conjecture" | "Let" |
+ "CoInductive" | "Record" | "Structure" |
"Inductive" | "Parameter" | "Theorem" |
"Variable" | "Variables"