aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml2
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"
]