coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Implement uniform parameters in ComInductive	Jasper Hugunin	2018-07-01
\| \| \| \|	Don't allow notations attached to uniform inductives
*	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \| \| \|	This API is a bit strange, I expect it will change at some point.
*	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\
\| *	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
\| \|
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-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.