aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/BinNat.v
Commit message (Expand)AuthorAge
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.Gravatar emakarov2007-11-08
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0...Gravatar emakarov2007-11-07
* Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.Gravatar emakarov2007-11-07
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* Changed the definition of Nminus in BinNat.v by removing comparison.Gravatar emakarov2007-09-20
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* Added the following theorems to BinPos:Gravatar emakarov2007-03-30
* qq proprietes de plus sur NcompareGravatar letouzey2006-04-29
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* ajout Pnat (suite)Gravatar herbelin2003-11-21
* Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...Gravatar herbelin2003-11-21
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
* NotationsGravatar herbelin2003-11-05
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...Gravatar herbelin2003-11-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 05:20:29 +0000