coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-08-25	Modify Structures/Orders.v to compile with -mangle-names	Jasper Hugunin
2020-03-23	Fix levels of `<=?` and `<?` in the stdlib	Jason Gross
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-11-14	Deprecate hint declaration/removal with no specified database	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-07-09	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey
2011-06-20	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey
2011-03-17	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey
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-07-10	Bool: iff lemmas about or, a reflect inductive, an is_true function	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-02-16	Uniformisation Sorting/Mergesort and Structures/Orders	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey