| Commit message (Expand) | Author | Age |
* | 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-07 |
* | 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-05 |
* | Moving never-used comments from Zhints.v to dev/doc so as not to | herbelin | 2011-10-01 |
* | 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 |