aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingGravatar glondu2011-08-17
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Cleanup in SpecViaZGravatar letouzey2011-06-30
* Cleanup of NdigitsGravatar letouzey2011-06-30
* 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
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* Numbers: a particular case of div_uniqueGravatar letouzey2011-06-24
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* 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
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Some simplifications in NZDomainGravatar letouzey2011-06-20
* Modularization of BinInt, related fixes in the stdlibGravatar 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
* Fix generated script for NMake, a rewrite necessitates full conversion forGravatar msozeau2011-04-18
* Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)Gravatar letouzey2011-03-30
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditionsGravatar letouzey2011-03-10
* BigQ : setting correct arguments scopesGravatar letouzey2011-02-23
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* 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
* f_equiv : a clone of f_equal that handles setoid equivalencesGravatar letouzey2011-01-04
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* NPeano.modulo : another trick a la "minus" for having a decreasing argGravatar letouzey2010-12-17
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* Nicer log2 function for nat (suggested by Hugo)Gravatar letouzey2010-12-17
* First release of Vector library.Gravatar pboutill2010-12-10
* 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
* NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrtGravatar 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
* Oups, fix last commit, a missing file in a vo.itargetGravatar letouzey2010-11-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-05 03:45:04 +0000