highlight

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 17 deletions

diff --git a/ide/highlight.mll b/ide/highlight.mll
index 9c0e5abee..4bc200ada 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -29,27 +29,19 @@ let identchar =
 let ident = firstchar identchar*
 
 let keyword = 
-  "Add" | "AddPath" | "Chapter" | "Check" | 
-  "CoInductive" |  "Compile" | "Defined" | 
-  "End" | "Export" | "Extraction" | "Fact" | "Fix" | "Global" | 
-  "Grammar" | "Hint" |
-  "Hints" | ("Hints" space+ "Resolve") |
-  "Immediate" | "Implicits" | "Import" | 
-  "Infix" | "Load" | "LoadPath" | "Local" | 
-  "Match" | "Module" | "Module Type" |
-  "Mutual" | "Print" | "Proof" | "Qed" |
-  "Record" | "Recursive" | 
-  ("Require" (space+ "Export")? space+ ident) | "Save" | "Scheme" |
-  "Section" | "Show" | "Syntactic" | "Syntax" | "Tactic" |
-  "Unset" |
-  ("Set" space+ "Implicit" space+ "Arguments") |
-  ("Implicit" space+ "Arguments" space+ ("On" | "Off")) | "Cases"
+  "Add" | "CoInductive" | "Defined" | 
+  "End" | "Export" | "Extraction" | "Hint" |
+  "Implicits" | "Import" | 
+  "Infix" | "Load" | "match" | "Module" | "Module Type" |
+  "Proof" | "Qed" |
+  "Record" | "Require" | "Save" | "Scheme" |
+  "Section" | "Unset" |
+  "Set"  
 
 let declaration = 
   "Lemma" | "Axiom" | "CoFixpoint" | "Definition"  |
-  ("Tactic" space+ "Definition") |
   "Fixpoint" | "Hypothesis" | 
-  "Inductive" | "Parameter" | "Remark" |  "Theorem" | 
+  "Inductive" | "Parameter" | "Theorem" | 
   "Variable" | "Variables" 
 
 rule next_order = parse