coq - The formal proof system

Age	Commit message (Expand)	Author
2020-03-19	[stdlib] Remove a few `auto with *`	Vincent Laporte
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-01-23	Pass some files to strict focusing mode.	Gaëtan Gilbert
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
2012-08-08	Updating headers.	herbelin
2011-01-03	Numbers: some improvements in proofs	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-01-11	Support "Local Obligation Tactic" (now the default in sections).	msozeau
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-15	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-21	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau
2008-09-14	Use manual implicts in Classes and rationalize class parameter names.	msozeau
2008-06-27	Enhanced discrimination nets implementation, which can now work with	msozeau
2008-05-11	- Cleanup parsing of binders, reducing to a single production for all	msozeau
2008-04-09	Fixes in new Morphisms files.	msozeau
2008-04-08	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau