index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
PArith
/
Pnat.v
Commit message (
Expand
)
Author
Age
*
Update headers.
Maxime Dénès
2015-01-12
*
eta contractions
Pierre Boutillier
2014-10-01
*
Simpl less (so that cbn will not simpl too much)
Pierre Boutillier
2014-10-01
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
Pos.iter arguments in a better order for cbn.
Pierre Boutillier
2014-05-02
*
Pos.compare_cont takes the comparison as first argument
Pierre Boutillier
2014-02-28
*
nat_iter n f x -> nat_rect _ x (fun _ => f) n
pboutill
2012-12-21
*
Updating headers.
herbelin
2012-08-08
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Modularisation of Znat, a few name changed elsewhere
letouzey
2011-05-05
*
Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)
letouzey
2011-05-05
*
Modularization of Pnat
letouzey
2011-05-05
*
Modularization of BinPos + fixes in Stdlib
letouzey
2011-05-05
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
*
Add small utility lemmas about nat/P/Z/Q arithmetic.
letouzey
2010-11-02
*
Move stuff about positive into a distinct PArith subdir
letouzey
2010-11-02