| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v. |  emakarov | 2007-11-07 |
| * | Replaced BinNat with a new version that is based on theories/Numbers/Natural/... | emakarov | 2007-11-07 |
| * | In agreement with Laurent Thery, start migration of auxiliary results |  letouzey | 2007-11-01 |
| * | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov | 2007-10-16 |
| * | Added the compilation of theories/Numbers to Makefile.common. The following t... | emakarov | 2007-10-01 |
| * | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov | 2007-09-20 |
| * | A generic preprocessing tactic zify for (r)omega | letouzey | 2007-07-18 |
| * | Extension of NArith: Nminus, Nmin, etc | letouzey | 2007-06-07 |
| * | Réparation de NArith/BinPos.v suite au commit #9739 |  notin | 2007-04-02 |
| * | Added the following theorems to BinPos: | emakarov | 2007-03-30 |
| * | Removed an unnecessary argument (p : positive) in Prect_base. | emakarov | 2007-03-14 |
| * | Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à |  herbelin | 2006-12-28 |
| * | Remplacement de la définition de Pind et Prec par une définition | herbelin | 2006-12-28 |
| * | Changement dans ring et field, beaucoup de correction d'erreurs, |  bgregoir | 2006-12-15 |
| * | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom |  barras | 2006-10-05 |
| * | qq proprietes de plus sur Ncompare | letouzey | 2006-04-29 |
| * | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin | 2006-04-28 |
| * | suite du pont entre Bvector et N | letouzey | 2006-04-26 |
| * | Un gros coup de lifting pour IntMap: | letouzey | 2006-04-25 |
| * | ouverture du bon scope (positive_scope) derriere le constructeur Npos de N | letouzey | 2006-04-06 |
| * | Minimum pour documentation TeX de la biblio | herbelin | 2006-02-22 |
| * | Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours... |  coq | 2005-02-07 |
| * | Suppression de l'Unboxed des opérations sur positive (cf bug 898) | herbelin | 2005-02-04 |
| * | Changement dans les boxed values . |  gregoire | 2004-11-12 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras | 2003-12-15 |
| * | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
| * | Report de lemmes de Znumtheory dans Zabs ou BinInt | herbelin | 2003-11-29 |
| * | ajout Pnat (suite) | herbelin | 2003-11-21 |
| * | Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e... | herbelin | 2003-11-21 |
| * | Pour les .v8 | herbelin | 2003-11-14 |
| * | Presentation | herbelin | 2003-11-14 |
| * | Ordre standard pour l'associativite | herbelin | 2003-11-14 |
| * | Noms/énoncés plus canoniques | herbelin | 2003-11-12 |
| * | Independance vis a vis noms variables liees | herbelin | 2003-11-12 |
| * | Notations | herbelin | 2003-11-05 |
| * | Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif... | herbelin | 2003-11-05 |
emakarov
letouzey
notin
herbelin
bgregoir
barras
coq
gregoire