coq - The formal proof system

Age	Commit message (Collapse)	Author
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

2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
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.