diff options
Diffstat (limited to 'tools/coqdoc/index.mll')
| -rw-r--r-- | tools/coqdoc/index.mll | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 9525b457e0..d12b1fe88e 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -189,6 +189,8 @@ rule traverse = parse | "Inductive" space { current_type := Inductive; index_ident lexbuf; inductive lexbuf; traverse lexbuf } + | "Record" space + { current_type := Inductive; index_ident lexbuf; traverse lexbuf } | "Module" (space+ "Type")? space { current_type := Module; index_ident lexbuf; traverse lexbuf } (*i*** |