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-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-03-30	Error when [foo.(bar)] is used with nonprojection [bar]	Gaëtan Gilbert
2018-12-19	Put #[universes(template)] on all auto template spots in stdlib	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
2016-06-16	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau
2014-05-09	Restore implicit arguments of irreflexivity (fixes bug #3305).	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
2012-07-09	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2010-07-05	FSets/Msets: some renaming of module params to simplify the task of the extra...	letouzey
2010-06-16	MSetInterface: no induction principle about a Record (nicer extraction)	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
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-07	Include can accept both Module and Module Type	letouzey
2010-01-07	MSetInterface: more modularity	letouzey
2010-01-05	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-11-30	Fix backtracking heuristic in typeclass resolution.	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-21	MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect	letouzey
2009-10-16	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey
2009-10-15	MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)	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