coq - The formal proof system

Age	Commit message (Expand)	Author
2011-10-10	Proper fix for complement/flip instances.	msozeau
2011-10-07	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey
2011-10-07	Fix bug #2557 and an issue with Propers for complement	msozeau
2011-10-07	Improved handling of element equalities in fsetdec (fix #2467)	letouzey
2011-10-05	Removing vernacular code mistakenly committed.	herbelin
2011-10-05	Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...	letouzey
2011-10-01	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin
2011-09-17	Euclid: make the proof transparent (example of extraction in stdlib)	letouzey
2011-09-16	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey
2011-09-06	Avoid registering λ and Π as keywords just for some private Local Notation	letouzey
2011-09-02	Bug 2589: Documentation patch of Hendrik Tews	pboutill
2011-08-23	Use of the standard terminology for Diaconescu's theorem (not "paradox").	herbelin
2011-08-17	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-11	SearchAbout and similar: add a customizable blacklist	letouzey
2011-08-10	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-09	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-08	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-07-26	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-16	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-04	StrictOrder marked explicitly to be in Prop	letouzey
2011-07-01	Some cleanup of Zcomplements	letouzey
2011-07-01	Cleanup of files related with power over Z.	letouzey
2011-06-30	Cleanup in SpecViaZ	letouzey
2011-06-30	Cleanup of Ndigits	letouzey
2011-06-28	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-27	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-24	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-23	cleanup of Zsgn	letouzey
2011-06-23	cleanup of Zmin and Zmax	letouzey
2011-06-23	Some more cleanup of Zorder	letouzey
2011-06-21	Follow-up concerning eqb / ltb / leb comparisons	letouzey
2011-06-20	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