aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/PArith
Commit message (Expand)AuthorAge
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Peano recursion for positive: integration of Daniel Schepler's codeGravatar letouzey2011-05-05
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* BinNatDef containing all functions of BinNat, misc adaptations in BinPosGravatar letouzey2011-05-05
* BinPosDef: a module with all code about positive, later Included in BinPosGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Modularization of PnatGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Fixed a bug of destruct which was sometimes forgetting local definitions behi...Gravatar herbelin2011-04-24
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* First release of Vector library.Gravatar pboutill2010-12-10
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02