diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:10:19 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:10:19 +0000 |
| commit | aff2ab6c9ae4d1705903717840c0ba83c80fe3c5 (patch) | |
| tree | 94acd53777c61aed016146172755bd37c050fc1e /tools/coqdoc/output.ml | |
| parent | d2923f2800a951b12f6964fc3449a7682569f25c (diff) | |
Add some keyword
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10480 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 647cc5da3..3e171a2c5 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -31,9 +31,9 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; + [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint"; + "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Immediate"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; @@ -48,7 +48,7 @@ let is_keyword = "Arguments"; "Instance"; "Class"; "where"; "Instantiation"; (* Program *) - "Program Definition"; "Program Fixpoint"; "Program Lemma"; + "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; "Program Instance"; (*i (* correctness *) |