index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
ZArith
/
Zmin.v
Commit message (
Expand
)
Author
Age
*
ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType
letouzey
2010-02-09
*
Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...
letouzey
2010-01-07
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.
herbelin
2009-10-04
*
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-28
*
Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.
herbelin
2009-09-27
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
A generic preprocessing tactic zify for (r)omega
letouzey
2007-07-18
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
Mise en forme des theories
notin
2006-10-17
*
Nettoyage Zmin.v, création Zmax.v et Zminmax.v
herbelin
2006-02-12
*
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 lemmes; independance vis a vis noms variables liees
herbelin
2003-11-12
*
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...
herbelin
2003-11-05