aboutsummaryrefslogtreecommitdiff
path: root/theories/PArith
AgeCommit message (Expand)Author
2011-05-05Peano recursion for positive: integration of Daniel Schepler's codeletouzey
2011-05-05Modularisation of Znat, a few name changed elsewhereletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-05-05BinNatDef containing all functions of BinNat, misc adaptations in BinPosletouzey
2011-05-05BinPosDef: a module with all code about positive, later Included in BinPosletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of Pnatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions behi...herbelin
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-10First release of Vector library.pboutill
2010-12-09In passing, very quick uniformization of coqdoc headers in a few files.herbelin
2010-12-06Numbers and bitwise functions.letouzey
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
2010-11-05Numbers: axiomatization, properties and implementations of gcdletouzey
2010-11-02Add small utility lemmas about nat/P/Z/Q arithmetic.letouzey
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey