coq - The formal proof system

Age	Commit message (Expand)	Author
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
2013-11-02	Restore Zsqrt compat now that refine works fine with match.	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	aspiwack
2013-07-17	More dynamic argument scopes	letouzey
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-21	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill
2012-12-18	No more constant named "int" in Coq theories (cf bug #2878)	letouzey
2012-08-08	Updating headers.	herbelin
2012-07-06	BinPos/BinInt/BinNat : fix some argument scopes	letouzey
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey