coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Support locality attributes for Hint Rewrite (including export)	Gaëtan Gilbert
2020-08-25	Modify Numbers/NatInt/NZGcd.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZDiv.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZLog.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZPow.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZParity.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZOrder.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZMul.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZAdd.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZBase.v to compile with -mangle-names	Jasper Hugunin
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-05-23	Fixing typos - Part 3	JPR
2019-01-23	Pass some files to strict focusing mode.	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-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-06-16	Remove unneded hints in NZGcd	Matthieu Sozeau
2016-06-16	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-07	Fix some typos.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-07-09	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey
2014-05-20	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot
2014-05-06	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-07-17	More dynamic argument scopes	letouzey
2013-02-13	make validate repaired via a temporary fix for #2949	letouzey
2012-12-21	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill
2012-12-18	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey
2012-08-08	Updating headers.	herbelin
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2011-08-11	SearchAbout and similar: add a customizable blacklist	letouzey
2011-07-01	Cleanup of files related with power over Z.	letouzey
2011-06-24	Numbers: a particular case of div_unique	letouzey
2011-06-24	Numbers: change definition of divide (compat with Znumtheory)	letouzey
2011-06-23	Some more cleanup of Zorder	letouzey
2011-06-20	Some migration of results from BinInt to Numbers	letouzey
2011-06-20	Some simplifications in NZDomain	letouzey
2011-02-11	Annotations at functor applications:	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-20	Numbers: simplier spec for testbit	letouzey
2011-01-04	f_equiv : a clone of f_equal that handles setoid equivalences	letouzey
2011-01-03	Numbers: some improvements in proofs	letouzey
2010-12-17	Cosmetic : let's take advantage of the n-ary exists notation	letouzey
2010-12-06	Numbers and bitwise functions.	letouzey