aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-11-27 14:39:35 +0000
committerherbelin2004-11-27 14:39:35 +0000
commitc819cf9cc0b99cec495f33d40a82c9a7bc84eb91 (patch)
tree548f136bc7b46f9502d307734d90ff2ecbfba731
parentf6c57e62abb2b208bafbcc12c4b8afd742b82474 (diff)
Complétion déclarations coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6362 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/highlight.mll7
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll
index ea40821466..baedaf0fb4 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -21,12 +21,12 @@
let is_keyword =
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ())
- [ "Add" ; "CoInductive" ; "Defined" ;
+ [ "Add" ; "Defined" ;
"End" ; "Export" ; "Extraction" ; "Hint" ; "Hints" ;
"Implicits" ; "Import" ;
"Infix" ; "Load" ; "match" ; "Module" ;
"Proof" ; "Qed" ;
- "Record" ; "Require" ; "Save" ; "Scheme" ;
+ "Require" ; "Save" ; "Scheme" ;
"Section" ; "Unset" ;
"Set" ; "Notation"
];
@@ -37,6 +37,9 @@
List.iter (fun s -> Hashtbl.add h s ())
[ "Lemma" ; "Axiom" ; "CoFixpoint" ; "Definition" ;
"Fixpoint" ; "Hypothesis" ;
+ "Hypotheses" ; "Axioms" ; "Parameters" ; "Subclass" ;
+ "Remark" ; "Fact" ; "Conjecture" ; "Let" ;
+ "CoInductive" ; "Record" ; "Structure" ;
"Inductive" ; "Parameter" ; "Theorem" ;
"Variable" ; "Variables"
];