diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d4c396d49..8c0e7e05a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -375,7 +375,7 @@ let vernac_assumption kind l nl= let vernac_inductive f indl = if Dumpglob.dump () then List.iter (fun ((lid, _, _, cstrs), _) -> - Dumpglob.dump_definition lid false"ind"; + Dumpglob.dump_definition lid false "ind"; List.iter (fun (_, (lid, _)) -> Dumpglob.dump_definition lid false "constr") cstrs) indl; |