diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 13:48:46 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 13:58:38 +0200 |
| commit | d065ea30843729c70e3b501a331d11499ad197e7 (patch) | |
| tree | 6533a27ab527ba54047d9eb123d31579752622e0 /tools/coqdoc/output.ml | |
| parent | e260172f03f792a388797f066438e079290074d0 (diff) | |
Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 6f853926f..28480d4bd 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -59,7 +59,7 @@ let is_keyword = "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; "fix"; "cofix"; (* Ltac *) - "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; (* Notations *) "level"; "associativity"; "no" ] |