coq - The formal proof system

Age	Commit message (Expand)	Author
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias
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-07	Improve field_simplify on fractions with constant denominator	thery
2019-03-30	Error when [foo.(bar)] is used with nonprojection [bar]	Gaëtan Gilbert
2019-02-28	Implement a method for manual declaration of implicits.	Jasper Hugunin
2018-12-19	Put #[universes(template)] on all auto template spots in stdlib	Gaëtan Gilbert
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-10-15	[stdlib] Fix warnings on deprecated `Add Setoid`	Emilio Jesus Gallego Arias
2017-10-05	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-09-27	Keyed unification option, compiling the whole standard library	Matthieu Sozeau
2014-05-06	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau
2014-05-06	Try a new way of handling template universe levels	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-11-21	Field_theory: nicer notations for constants 0 1 ...	Pierre Letouzey
2013-08-23	Fixing an incompleteness of the ring/field tactics	amahboub
2013-08-22	Correcting misplaced Proof command.	amahboub
2013-08-22	Fixing a significant efficiency leak in the code of the field tactic.	amahboub
2013-08-22	Field_theory : faster and nicer proofs + nice notations.	letouzey
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-10-26	Change Hint Resolve, Immediate to take a global reference as argument	msozeau
2012-08-08	Updating headers.	herbelin
2012-07-19	Getting rid of the undocumented [complete] tactic, which was	ppedrot
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2011-06-21	Follow-up concerning eqb / ltb / leb comparisons	letouzey
2011-05-05	BinInt: Z.add become the alternative Z.add'	letouzey
2011-05-05	Modularization of BinInt, related fixes in the stdlib	letouzey
2011-05-05	Setoid_ring: some cleanups related with BinPos and BinNat	letouzey
2011-05-05	Modularization of BinPos + fixes in Stdlib	letouzey
2010-10-21	Still some more Cpow in Type rather than Set (cf. r13542)	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey