coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	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-17
*	eta contractions	Pierre Boutillier	2014-10-01
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to	Hugo Herbelin	2014-08-18
*	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin	2014-08-05
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Pos.iter arguments in a better order for cbn.	Pierre Boutillier	2014-05-02
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-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-11-02
*	More dynamic argument scopes	letouzey	2013-07-17
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Updating headers.	herbelin	2012-08-08
*	BinPos/BinInt/BinNat : fix some argument scopes	letouzey	2012-07-06
*	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-07-05
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
*	Functions *_beq aren't generated anymore, remove comments about them	letouzey	2012-05-30
*	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-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	Deleted the only use of BeginSubProof from the standard library.	ppedrot	2012-01-23
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	BinInt: more structured scripts thanks to bullets and { }	letouzey	2011-08-09
*	Some cleanup of Zcomplements	letouzey	2011-07-01
*	Cleanup of files related with power over Z.	letouzey	2011-07-01
*	Deletion of useless Zdigits_def	letouzey	2011-06-28
*	Deletion of useless Zlog_def	letouzey	2011-06-28
*	Deletion of useless Zsqrt_def	letouzey	2011-06-28
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	Some cleanup of Wf_Z.v	letouzey	2011-06-28
*	Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)	letouzey	2011-06-27
*	Znumtheory: a correct version of a compatibility Zdivide_intro	letouzey	2011-06-27
*	Clean-up of Znumtheory, deletion of Zgcd_def	letouzey	2011-06-24
*	Numbers: change definition of divide (compat with Znumtheory)	letouzey	2011-06-24
*	cleanup of Zsgn	letouzey	2011-06-23
*	cleanup of Zmin and Zmax	letouzey	2011-06-23