summaryrefslogtreecommitdiff
path: root/ide/highlight.mll
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commit6497f27021fec4e01f2182014f2bb1989b4707f9 (patch)
tree473be7e63895a42966970ab6a70998113bc1bd59 /ide/highlight.mll
parent6b649aba925b6f7462da07599fe67ebb12a3460e (diff)
Imported Upstream version 8.0pl2upstream/8.0pl2
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"