| Commit message (Expand) | Author | Age |
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Testing a replacement of "cut" by "enough" on a couple of test files. | Hugo Herbelin | 2014-08-05 |
* | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey | 2014-07-09 |
* | Updating headers. | herbelin | 2012-08-08 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | Notation: a new annotation "compat 8.x" extending "only parsing" | letouzey | 2012-07-05 |
* | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def | letouzey | 2011-06-28 |
* | 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 |
* | Zdiv: results about eqm (the equality modulo some N) under a section | letouzey | 2011-05-05 |
* | 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 |
* | Add small utility lemmas about nat/P/Z/Q arithmetic. | 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 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Numbers: properties of min/max with respect to 0,S,P,add,sub,mul | letouzey | 2010-02-09 |
* | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey | 2010-02-09 |
* | Support "Local Obligation Tactic" (now the default in sections). | msozeau | 2010-01-11 |
* | Numbers abstract layer: more Module Type, used especially for divisions. | letouzey | 2010-01-05 |
* | Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/Numbers | letouzey | 2010-01-05 |
* | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
* | Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation | letouzey | 2008-10-20 |
* | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey | 2008-05-27 |
* | Fix bugs that were reopened due to the change of setoid | msozeau | 2008-03-08 |
* | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
* | one forgotten compatibility lemma | letouzey | 2008-02-08 |
* | Adding Zdiv_le_compat_l | thery | 2008-01-22 |
* | A result about Zsgn(a/b), both for Zdiv and ZOdiv | letouzey | 2007-11-10 |
* | First reasonably complete version of ZOdiv, including some properties | letouzey | 2007-11-10 |
* | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey | 2007-11-08 |
* | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey | 2007-11-06 |
* | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey | 2007-11-06 |
* | Adding Qround.v (and helper lemmas and hints) | roconnor | 2007-11-01 |
* | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor | 2007-10-19 |
* | normalisation (by closure) was not performed under fixpoints | barras | 2007-07-12 |
* | Mise en forme des theories | notin | 2006-10-17 |
* | commit de field + renommages | barras | 2006-09-26 |
* | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras | 2006-09-26 |
* | Changement dans les boxed values . | gregoire | 2004-11-12 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |