| Commit message (Expand) | Author | Age |
* | Updating headers. | herbelin | 2012-08-08 |
* | SearchAbout and similar: add a customizable blacklist | letouzey | 2011-08-11 |
* | Numbers: a particular case of div_unique | letouzey | 2011-06-24 |
* | Numbers: change definition of divide (compat with Znumtheory) | letouzey | 2011-06-24 |
* | ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditions | letouzey | 2011-03-10 |
* | Numbers and bitwise functions. | letouzey | 2010-12-06 |
* | Integer division: quot and rem (trunc convention) in addition to div and mod | letouzey | 2010-11-10 |
* | Numbers: NZPowProp as a Module Type, some module variable renaming | letouzey | 2010-11-02 |
* | Numbers: new functions pow, even, odd + many reorganisations | letouzey | 2010-10-14 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.S | letouzey | 2010-01-29 |
* | Numbers: axiomatization + generic properties of abs and sgn. | letouzey | 2010-01-08 |
* | Numbers: separation of funs, notations, axioms. Notations via module, without... | letouzey | 2010-01-07 |
* | "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ... | letouzey | 2010-01-06 |
* | Numbers abstract layer: more Module Type, used especially for divisions. | letouzey | 2010-01-05 |
* | Division in Numbers: proofs with less auto (less sensitive to hints, in parti... | letouzey | 2010-01-05 |
* | Division in Numbers: factorisation of signatures | letouzey | 2010-01-05 |
* | Specific syntax for Instances in Module Type: Declare Instance | letouzey | 2010-01-04 |
* | Division in Numbers : more properties, new filenames based on a paper by R. B... | letouzey | 2009-12-17 |