index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
ZArith
/
Znat.v
Commit message (
Expand
)
Author
Age
*
First release of Vector library.
pboutill
2010-12-10
*
Numbers and bitwise functions.
letouzey
2010-12-06
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
*
Integer division: quot and rem (trunc convention) in addition to div and mod
letouzey
2010-11-10
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)
herbelin
2010-03-28
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression
notin
2008-03-28
*
Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...
letouzey
2007-11-06
*
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
*
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
*
Restructuration ZArith
herbelin
2003-11-12