coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Support locality attributes for Hint Rewrite (including export)	Gaëtan Gilbert
2020-08-25	Modify Structures/OrdersFacts.v to compile with -mangle-names	Jasper Hugunin
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-05-23	Fixing typos - Part 3	JPR
2019-01-23	Pass some files to strict focusing mode.	Gaëtan Gilbert
2018-11-28	Merge PR #7153: Make OrderedTypeFullFacts a module functor	Gaëtan Gilbert
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-04-02	Make OrderedTypeFullFacts a module functor	Simon Gregersen
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