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 3e171a2c5..5a5f1e7bf 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -37,7 +37,7 @@ let is_keyword =
"Hypothesis"; "Hypotheses";
"Immediate"; "Implicit"; "Import"; "Inductive";
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
- "Module"; "Module Type"; "Declare Module";
+ "Module"; "Module Type"; "Declare Module"; "Include";
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
"Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";