coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-02	{new,setoid_}ring -> ring	Maxime Dénès
	I believe this renaming makes it easier for new contributors to discover the code of `ring`.
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-05-24	Stop using pstate in global print queries	Gaëtan Gilbert
	Using pstate makes no sense for printing global stuff
2019-03-27	[plugins] [setoid_ring] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias

2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
	This should make https://github.com/coq/coq/pull/9129 easier.
2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
	We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
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.