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
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
2016-11-24	Fix some documentation typos.	Guillaume Melquiond
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-02	Eta contractions to please cbn	Pierre Boutillier
2012-10-26	Change Hint Resolve, Immediate to take a global reference as argument	msozeau
2012-07-09	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-12	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey
2010-01-05	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey
2009-11-15	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau
2009-11-08	Use generalizable variables info when internalizing arbitrary bindings,	msozeau
2009-10-13	MSets: a new generation of FSets	letouzey