coq - The formal proof system

Age	Commit message (Expand)	Author
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
2012-07-05	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey
2012-06-19	BinInt: a forgotten scope for a notation	letouzey
2012-05-30	Functions *_beq aren't generated anymore, remove comments about them	letouzey
2012-04-15	Fixing typo in previous commit r15180.	herbelin
2012-04-15	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin
2012-04-13	MSetRBT : implementation of MSets via Red-Black trees	letouzey
2012-01-23	Deleted the only use of BeginSubProof from the standard library.	ppedrot
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-10-01	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin
2011-09-16	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey
2011-08-11	SearchAbout and similar: add a customizable blacklist	letouzey
2011-08-09	BinInt: more structured scripts thanks to bullets and { }	letouzey
2011-07-01	Some cleanup of Zcomplements	letouzey
2011-07-01	Cleanup of files related with power over Z.	letouzey
2011-06-28	Deletion of useless Zdigits_def	letouzey