| Age | Commit message (Expand) | Author |
|---|
| 2009-11-11 | Better compatibility for Peqb | letouzey |
| 2009-11-10 | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | 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-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2009-03-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
| 2008-06-01 | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey |
| 2008-04-14 | BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanup | letouzey |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-02-10 | Proposal of a nice notation for constructors xI and xO of type positive | letouzey |
| 2007-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 2007-10-16 | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov |
| 2007-09-20 | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov |
| 2007-07-18 | A generic preprocessing tactic zify for (r)omega | letouzey |
| 2007-06-07 | Extension of NArith: Nminus, Nmin, etc | letouzey |
| 2007-04-02 | Réparation de NArith/BinPos.v suite au commit #9739 | notin |
| 2007-03-30 | Added the following theorems to BinPos: | emakarov |
| 2007-03-14 | Removed an unnecessary argument (p : positive) in Prect_base. | emakarov |
| 2006-12-28 | 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 |
| 2005-02-07 | Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours... | coq |
| 2005-02-04 | Suppression de l'Unboxed des opérations sur positive (cf bug 898) | herbelin |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-11-29 | 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-21 | Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e... | herbelin |
| 2003-11-14 | Presentation | herbelin |
| 2003-11-12 | Independance vis a vis noms variables liees | herbelin |
| 2003-11-05 | Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif... | herbelin |
