aboutsummaryrefslogtreecommitdiff
path: root/vernac/comDefinition.ml
AgeCommit message (Collapse)Author
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-21Merge code paths in interp_definition and cleanup a bit.Gaëtan Gilbert
2017-12-18[vernac] Cleanup of do_definition.Emilio Jesus Gallego Arias
We remove a few old-style normalization and try to use the newer APIs, however, it is hard to say whether the right magic is being used.
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
This is useful as it allows to reflect program_mode behavior as an attribute.
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
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.