| Age | Commit message (Expand) | Author |
|---|
| 2008-04-27 | - Fix bug in unification not taking into account the right meta | msozeau |
| 2008-03-28 | Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression | notin |
| 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-03-04 | one more substitution s/Set/Type/ | letouzey |
| 2008-02-10 | Proposal of a nice notation for constructors xI and xO of type positive | letouzey |
| 2008-02-08 | one forgotten compatibility lemma | letouzey |
| 2008-01-24 | Keep the Z_scope local to this file. | roconnor |
| 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-09 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0... | jforest |
| 2007-11-09 | more about ZOdiv and ZOmod (still not finished) | 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-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 2007-10-19 | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor |
| 2007-08-08 | Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v | emakarov |
| 2007-07-18 | A generic preprocessing tactic zify for (r)omega | letouzey |
| 2007-07-12 | normalisation (by closure) was not performed under fixpoints | barras |
| 2007-04-12 | Transparency of Z_lt_le_dec | notin |
| 2006-12-12 | Bug nommage Zgt_trans_succ | herbelin |
| 2006-12-11 | correction Open Local Scope (Ring) | bgregoir |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-10-30 | fixed field_simplify + changed precedence of let and fun in ltac | barras |
| 2006-10-27 | simplif de la partie ML de ring/field | barras |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-10-05 | revert, the previous commit was a mistake | bertot |
| 2006-10-05 | A version of natprering that should be more efficient and removal of a bad | bertot |
| 2006-10-05 | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom | barras |
| 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 |
| 2006-06-26 | Ajout de Zgcd_spec (compat.) | notin |
| 2006-06-25 | nouvel algorithme pour Zgcd (plus rapide) + un Qcompare | letouzey |
| 2006-06-09 | Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT... | herbelin |
| 2006-05-31 | ajout de QArith dans les theories standards | letouzey |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-05-23 | Changement de précédence de l'argument du by de assert; conséquences... | herbelin |
| 2006-05-14 | On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos | letouzey |
| 2006-05-13 | typo | letouzey |
| 2006-05-13 | un Zgcd calculant dans coq | letouzey |
| 2006-05-11 | une fonction pouvant calculer le gcd en coq | letouzey |
| 2006-05-05 | un Zgcd general gardant trace des coefs | letouzey |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-02-12 | Bug Scope | herbelin |
| 2006-02-12 | Nettoyage Zmin.v, création Zmax.v et Zminmax.v | herbelin |
| 2005-05-02 | Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p... | herbelin |
| 2005-05-02 | Lemme de passage de l'autre côté d'une égalité | herbelin |
