coq - The formal proof system

Age	Commit message (Expand)	Author
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2016-10-12	Little addition to 6eede071 for consistency of style in OrdersFacts.v.	Hugo Herbelin
2016-09-17	Further "decide equality" tests on demand of Jason.	Hugo Herbelin
2016-09-15	Extending "contradiction" so that it recognizes statements such as "~x=x" or ...	Hugo Herbelin
2015-12-31	Put implicits back as in 8.4.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2011-06-21	Follow-up concerning eqb / ltb / leb comparisons	letouzey
2011-06-20	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2010-07-18	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-02-12	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey