coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Euclid: make the proof transparent (example of extraction in stdlib)	letouzey	2011-09-17
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	Avoid registering λ and Π as keywords just for some private Local Notation	letouzey	2011-09-06
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	Use of the standard terminology for Diaconescu's theorem (not "paradox").	herbelin	2011-08-23
*	Give inner fixpoint of gcd31 a name, to avoid excessive unfolding	glondu	2011-08-17
*	Smaller proof terms for QcPower_{0,pos}	glondu	2011-08-17
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Take benefit of bullets available by default in Prelude	herbelin	2011-08-10
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	BinInt: more structured scripts thanks to bullets and { }	letouzey	2011-08-09
*	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack	2011-08-09
*	Some forgotten lemma in Arith with "O" in the name instead of "0".	herbelin	2011-08-08
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	All the parameters of Compare are implicits.	pboutill	2011-07-26
*	All the parameters of or can be implicits.	pboutill	2011-07-26
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Some facts about functional extensionality (especially alternative	herbelin	2011-07-16
*	More lemmas relating the different equivalent formulations of eq_dep.	herbelin	2011-07-16
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Added a characterization of unique existence.	herbelin	2011-07-16
*	StrictOrder marked explicitly to be in Prop	letouzey	2011-07-04
*	Some cleanup of Zcomplements	letouzey	2011-07-01
*	Cleanup of files related with power over Z.	letouzey	2011-07-01
*	Cleanup in SpecViaZ	letouzey	2011-06-30
*	Cleanup of Ndigits	letouzey	2011-06-30
*	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: a particular case of div_unique	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
*	Some more cleanup of Zorder	letouzey	2011-06-23
*	Follow-up concerning eqb / ltb / leb comparisons	letouzey	2011-06-21
*	Some migration of results from BinInt to Numbers	letouzey	2011-06-20
*	Zcompare.destr_zcompare subsumed by case Z.compare_spec	letouzey	2011-06-20
*	Clean-up of Zcompare and Zorder	letouzey	2011-06-20
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Some simplifications in NZDomain	letouzey	2011-06-20
*	Making printing of backtick in Program reparsable (avoiding collision with "`(")	herbelin	2011-06-14
*	Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.	msozeau	2011-06-07
*	BinNat: N.binary_rect is now a definition instead of an opaque proof	letouzey	2011-05-05
*	Peano recursion for positive: integration of Daniel Schepler's code	letouzey	2011-05-05
*	Minimal lemmas about Z.gt, N.gt and co	letouzey	2011-05-05