aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comInductive.ml
Commit message (Collapse)AuthorAge
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
* [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.