coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-03-28	Patterns: Accepting patterns in PFix and PCofix and not only constr.	Hugo Herbelin

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

2018-01-30	Use r.(p) syntax to print primitive projections.	Maxime Dénès
	There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
	We do up to `Term` which is the main bulk of the changes.
2017-10-25	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias
	To this extent we factor out the relevant bits to a new file, ltac_pretype.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-07	Put all plugins behind an "API".	Matej Kosik