diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-20 02:05:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-20 15:03:51 +0200 |
| commit | 9452f9a3b3bee737c3b4b687e1601eb4ca45b298 (patch) | |
| tree | 9960fdd57b4b6404e616204b7095c7fbe1d02613 /tools/coqdoc | |
| parent | b7cf93cec115b61889e31c0abefdbd29d9b51ebe (diff) | |
[coqdoc] Add keywords in bug 2884.
Diffstat (limited to 'tools/coqdoc')
| -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 82d3d62b5..e06ef9d76 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -36,7 +36,7 @@ let is_keyword = "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; "Implicit"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; @@ -58,9 +58,9 @@ let is_keyword = (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; - "fix"; "cofix"; + "fix"; "cofix"; "is"; (* Ltac *) - "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec"; (* Notations *) "level"; "associativity"; "no" ] @@ -70,7 +70,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; + "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; |