coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-19	Fix #9595: missing non-primitive-record warning with 0 field record	Gaëtan Gilbert

2018-12-19	warn when using auto template, funind never uses template poly	Gaëtan Gilbert
	The warning can be avoided with the attributes, (or just disable the warning itself I guess).
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
	This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-09-19	Fix #7754: universe declarations on mutual inductives	Gaëtan Gilbert

2018-09-13	Add option to control automatic template polymorphism.	Gaëtan Gilbert

2018-09-13	Add explicit atribute for template polymorphism.	Gaëtan Gilbert

2018-07-01	Implement uniform parameters in ComInductive	Jasper Hugunin
	Don't allow notations attached to uniform inductives
2018-05-17	Split off Universes functions dealing with names.	Gaëtan Gilbert
	This API is a bit strange, I expect it will change at some point.
2018-03-07	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès

2018-03-05	Allow universe declarations for [with Definition].	Gaëtan Gilbert

2018-02-27	Update headers following #6543.	Théo Zimmermann

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.