diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 12:20:37 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 12:20:37 +0200 |
commit | 7d1cb9e0cbac64d91dcc8b71e8628f80746fff71 (patch) | |
tree | 9826fe106b2a0a8f150c048b996e774c1a61b9de | |
parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
parent | 9452f9a3b3bee737c3b4b687e1601eb4ca45b298 (diff) |
Merge PR#658: [coqdoc] Add keywords in bug 2884.
-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"; |