| Age | Commit message (Expand) | Author |
|---|
| 2010-02-09 | 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-01-11 | Support "Local Obligation Tactic" (now the default in sections). | msozeau |
| 2010-01-05 | 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 |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-09 | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey |
| 2008-10-20 | Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation | letouzey |
| 2008-05-27 | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey |
| 2008-03-08 | Fix bugs that were reopened due to the change of setoid | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2008-02-08 | one forgotten compatibility lemma | letouzey |
| 2008-01-22 | Adding Zdiv_le_compat_l | thery |
| 2007-11-10 | 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-08 | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey |
| 2007-11-06 | 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-01 | Adding Qround.v (and helper lemmas and hints) | roconnor |
| 2007-10-19 | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor |
| 2007-07-12 | normalisation (by closure) was not performed under fixpoints | barras |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-09-26 | commit de field + renommages | barras |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-13 | Require | herbelin |
| 2003-11-13 | qq petit ajouts à Zdiv | letouzey |
| 2003-09-21 | Changement de la politique de V8only: V8only tout seul signifie | herbelin |
| 2003-09-05 | Zdiv plus efficace: r+r -> 2*r | letouzey |
| 2003-04-09 | Ajout Open Scope | herbelin |
| 2003-04-09 | Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import". | herbelin |
| 2003-03-28 | Pas d'associativité gauche au niveau 3 en vieille syntaxe ! | herbelin |
| 2003-03-21 | *** empty log message *** | barras |
| 2003-03-12 | *** empty log message *** | barras |
| 2002-06-20 | ZArith_base, Zbool, Bool_nat | filliatr |
| 2002-06-05 | affaiblissement hyp de Zmult_reg_left | filliatr |
| 2002-05-14 | encore des lemmes sur Zdiv | filliatr |
| 2002-05-14 | nouveaux lemmes dans Zdiv (Claude Marche) | filliatr |
| 2002-04-19 | lemmes sur Zdiv/Zmod | filliatr |
| 2002-04-19 | un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F... | filliatr |
| 2002-04-17 | Uniformisation (Qed/Save et Implicits Arguments) | herbelin |
| 2002-04-08 | Zdiv -> Export ZArith | filliatr |
| 2002-04-08 | syntaxe pour Zdiv et Zmod | filliatr |
| 2002-04-05 | simplification preuve | filliatr |
| 2002-04-05 | nouveau module Zdiv | filliatr |
