| Commit message (Expand) | Author | Age |
|---|
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | Updating headers. |  herbelin | 2012-08-08 |
| * | ZArith + other : favor the use of modern names instead of compat notations |  letouzey | 2012-07-05 |
| * | theories/, plugins/ and test-suite/ ported to the Arguments vernacular |  gareuselesinge | 2011-11-21 |
| * | 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 |
| * | Clean-up of Znumtheory, deletion of Zgcd_def | letouzey | 2011-06-24 |
| * | Numbers: change definition of divide (compat with Znumtheory) | letouzey | 2011-06-24 |
| * | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey | 2011-06-20 |
| * | Modularization of BinInt, related fixes in the stdlib | letouzey | 2011-05-05 |
| * | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey | 2011-03-17 |
| * | Numbers: simplier spec for testbit | letouzey | 2011-01-20 |
| * | Cosmetic : let's take advantage of the n-ary exists notation | letouzey | 2010-12-17 |
| * | ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2 | letouzey | 2010-12-09 |
| * | 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: axiomatization, properties and implementations of gcd | letouzey | 2010-11-05 |
| * | NZSqrt : since spec is complete, no need for morphism axiom sqrt_wd | letouzey | 2010-11-02 |
| * | NZLog : since spec is complete, no need for morphism axiom log2_wd | letouzey | 2010-11-02 |
| * | Numbers : log2. Abstraction, properties and implementations. | letouzey | 2010-11-02 |
| * | Numbers: specs about sqrt and pow of neg numbers, even in NZ | letouzey | 2010-11-02 |
| * | Add sqrt in Numbers | letouzey | 2010-10-19 |
| * | Numbers : also axiomatize constants 1 and 2. | letouzey | 2010-10-14 |
| * | Numbers: new functions pow, even, odd + many reorganisations | letouzey | 2010-10-14 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | More improvements of BigN, BigZ, BigQ: | letouzey | 2010-01-18 |
| * | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey | 2010-01-17 |
| * | Numbers: two more Local Obligation Tactic | letouzey | 2010-01-12 |
| * | Numbers: BigN and BigZ get instantiations of all properties about div and mod | letouzey | 2010-01-08 |
| * | RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd | letouzey | 2009-12-18 |
| * | Fix backtracking heuristic in typeclass resolution. |  msozeau | 2009-11-30 |
| * | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey | 2009-11-12 |
| * | SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax | letouzey | 2009-11-10 |
| * | Simplification of Numbers, mainly thanks to Include | letouzey | 2009-11-10 |
| * | Numbers: more (syntactic) changes toward new style of type classes | letouzey | 2009-11-06 |
| * | Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc | letouzey | 2009-11-03 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Many fixes in unification: | msozeau | 2009-05-20 |
| * | Even better test for choosing rewrite or setoid_rewrite. | msozeau | 2008-07-26 |
| * | In abstract parts of theories/Numbers, plus/times becomes add/mul, | letouzey | 2008-06-03 |
| * | In abstract parts of theories/Numbers, plus/times becomes add/mul, | letouzey | 2008-06-02 |
| * | Enhance the BigN and BigZ infrastructure: | letouzey | 2008-06-01 |
Maxime Dénès
herbelin
letouzey
gareuselesinge
msozeau
glondu