aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/index.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 9daec6b554..6a61571c68 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -420,7 +420,7 @@ and module_refs = parse
{
let type_of_string = function
- | "def" | "coe" | "subclass" | "canonstruc"
+ | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
| "ex" | "scheme" -> Definition
| "prf" | "thm" -> Lemma
| "ind" | "coind" -> Inductive