coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-23	Fixing typos - Part 3	JPR
2019-04-02	Remove -compat 8.7	Jason Gross
2019-03-14	BinInt: 3 lemmas about testbit, mod _ 2^, ones	Andres Erbsen
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-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-10-02	Update compat notations to be compat 8.7	Jason Gross
2018-09-11	Merge PR #8425: Deprecate romega in favor of lia	Pierre-Marie Pédrot
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-09-10	Deprecate romega in favor of lia.	Vincent Laporte
2018-08-31	Make Numeral Notation follow Import, not Require	Jason Gross
2018-08-31	Numeral Notation for nat	Pierre Letouzey
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-03-02	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-02-20	Decimal: simple representation of base-10 numbers	Pierre Letouzey
2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin
2017-07-26	Merge PR #845: Add Z.mod_div lemma to standard library.	Maxime Dénès
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-29	Fix Zmod_div.	Russell O'Connor
2017-06-29	Use forall for consistency	roconnor-blockstream
2017-06-29	Add Z.mod_div lemma to standard library.	Russell O'Connor
2017-06-01	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik
2017-03-03	Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.	Hugo Herbelin
2017-03-03	Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.	Hugo Herbelin
2017-03-03	Completing "few lemmas about Zneg" with lemmas also about Zpos.	Hugo Herbelin
2016-10-24	Remove v62 from stdlib.	Théo Zimmermann
2016-05-04	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-05-04	Int.v: simplify Jason's commit 5b4e3ace	Pierre Letouzey
2016-05-04	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey
2016-03-04	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-29	Move compatibility notations to their proper files	Jason Gross
2015-12-07	Fix some typos.	Guillaume Melquiond
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-04-02	ZArith/Int.v: some modernizations	Pierre Letouzey
2015-01-12	Update headers.	Maxime Dénès
2014-10-17	Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...	Hugo Herbelin
2014-10-17	Essai où assert_style n'est utilisé que si pas visuellement une équation;	Hugo Herbelin
2014-10-01	eta contractions	Pierre Boutillier
2014-10-01	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier
2014-08-18	Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to	Hugo Herbelin
2014-08-05	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin
2014-07-09	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey
2014-06-04	Make standard library independent of the names generated by	Hugo Herbelin
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-05-02	Pos.iter arguments in a better order for cbn.	Pierre Boutillier
2014-05-02	Eta contractions to please cbn	Pierre Boutillier