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
2016-04-27	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin
2016-04-27	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin
2014-05-06	Try a new way of handling template universe levels	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
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
2010-07-22	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin
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-04-09	Change definition of FSetList so that equality is Leibniz	glondu
2010-02-12	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey
2010-01-12	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	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-11-03	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-10-16	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey
2009-10-15	OrderedType2.order is slightly weaker since last commit, adapt accordingly	letouzey
2009-10-13	MSets: a new generation of FSets	letouzey