aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Expand)AuthorAge
...
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
* Fixing typo in previous commit r15180.Gravatar herbelin2012-04-15
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
* Deleted the only use of BeginSubProof from the standard library.Gravatar ppedrot2012-01-23
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* BinInt: more structured scripts thanks to bullets and { }Gravatar letouzey2011-08-09
* Some cleanup of ZcomplementsGravatar letouzey2011-07-01
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* Deletion of useless Zlog_defGravatar letouzey2011-06-28
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defGravatar letouzey2011-06-28
* Some cleanup of Wf_Z.vGravatar letouzey2011-06-28
* Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)Gravatar letouzey2011-06-27
* Znumtheory: a correct version of a compatibility Zdivide_introGravatar letouzey2011-06-27
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* cleanup of ZsgnGravatar letouzey2011-06-23
* cleanup of Zmin and ZmaxGravatar letouzey2011-06-23
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* Some migration of results from BinInt to NumbersGravatar letouzey2011-06-20
* Zcompare.destr_zcompare subsumed by case Z.compare_specGravatar letouzey2011-06-20
* Clean-up of Zcompare and ZorderGravatar letouzey2011-06-20
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Minimal lemmas about Z.gt, N.gt and coGravatar letouzey2011-05-05
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
* BinInt: Z.add become the alternative Z.add'Gravatar 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
* Modularization of BinNat + fixes of stdlibGravatar 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
* Zdiv: results about eqm (the equality modulo some N) under a sectionGravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Numbers: simplier spec for testbitGravatar letouzey2011-01-20
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* 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
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-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
* NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down a...Gravatar letouzey2010-11-18
* Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.Gravatar letouzey2010-11-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 13:06:05 +0000