coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-23	Relying on the abstract notion of streams with location for parsing.	Hugo Herbelin
	We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml).
2020-12-27	Make ssrtermkind algebraic instead of a char	Lasse Blaauwbroek

2020-05-03	Wrap ssr tactics into V82.tactic.	Pierre-Marie Pédrot
	Porting them is still to be done, but at least we don't rely on the wrapper everywhere.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-29	Tentatively providing a localization function to ad-hoc camlp5 parsers.	Pierre-Marie Pédrot

2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-02-06	Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.	Théo Zimmermann

2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot

2018-11-23	Only use Coq API in coqpp.	Pierre-Marie Pédrot

2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot
	Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.