diff options
Diffstat (limited to 'tools/coqdoc/index.ml')
| -rw-r--r-- | tools/coqdoc/index.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 980f805ef..3da8de072 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -273,9 +273,9 @@ let type_of_string = function | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma - | "ind" | "coind" -> Inductive + | "ind" | "variant" | "coind" -> Inductive | "constr" -> Constructor - | "rec" | "corec" -> Record + | "indrec" | "rec" | "corec" -> Record | "proj" -> Projection | "class" -> Class | "meth" -> Method |