| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-06-20 | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey |
| 2011-06-20 | Some simplifications in NZDomain | letouzey |
| 2011-06-14 | Making printing of backtick in Program reparsable (avoiding collision with "`(") | herbelin |
| 2011-06-07 | Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms. | msozeau |
| 2011-05-05 | 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 |
