coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-25	[proof using] Remove duplicate code, refactor.	Emilio Jesus Gallego Arias
	PR #13183 introduced quite a bit of duplicate code, we refactor it and expose less internals on the way. That should make the API more robust.
2020-11-02	attribute #[using] for Definition and Fixpoint	Enrico Tassi

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-12	Unify Set and Unset handling for options	Gaëtan Gilbert
	Not sure if the idetop.set_options was correctly changed, ocaml types pass at least.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-10-10	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert

2017-10-10	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias
	We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.