coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix cbn behavior wrt simpl no match	Pierre Boutillier	2014-10-01
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Better fix of e5c025	Pierre Boutillier	2014-08-05
*	Fix to make Coq compile, I think this should still be accepted.	Matthieu Sozeau	2014-08-03
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing an incompleteness of the ring/field tactics	amahboub	2013-08-23
*	Ring_polynom : shorter proof for Psub_ok	letouzey	2013-08-22
*	Updating headers.	herbelin	2012-08-08
*	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey	2012-07-07
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)	letouzey	2010-10-14
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20