diff options
| author | herbelin | 2004-11-27 14:39:35 +0000 |
|---|---|---|
| committer | herbelin | 2004-11-27 14:39:35 +0000 |
| commit | c819cf9cc0b99cec495f33d40a82c9a7bc84eb91 (patch) | |
| tree | 548f136bc7b46f9502d307734d90ff2ecbfba731 | |
| parent | f6c57e62abb2b208bafbcc12c4b8afd742b82474 (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.mll | 7 |
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" ]; |
