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-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-03-30	Error when [foo.(bar)] is used with nonprojection [bar]	Gaëtan Gilbert
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-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-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2010-12-06	Numbers and bitwise functions.	letouzey
2010-11-02	Numbers: NZPowProp as a Module Type, some module variable renaming	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-02-09	ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType	letouzey
2010-01-13	Try to avoid re-declaring Equivalence, especially for Logic.eq	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey