index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
NArith
/
BinNat.v
Commit message (
Expand
)
Author
Age
...
*
Replaced BinNat with a new version that is based on theories/Numbers/Natural/...
emakarov
2007-11-07
*
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
*
Extension of NArith: Nminus, Nmin, etc
letouzey
2007-06-07
*
Added the following theorems to BinPos:
emakarov
2007-03-30
*
qq proprietes de plus sur Ncompare
letouzey
2006-04-29
*
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
*
Changement dans les boxed values .
gregoire
2004-11-12
*
Nouvelle en-tête
herbelin
2004-07-16
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
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
*
Ordre standard pour l'associativite
herbelin
2003-11-14
*
Noms/énoncés plus canoniques
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
[prev]