aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* 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
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
* NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdGravatar letouzey2010-11-02
* NZLog : since spec is complete, no need for morphism axiom log2_wdGravatar letouzey2010-11-02
* Numbers: misc improvementsGravatar letouzey2010-11-02
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* NPeano: A log2 function for natGravatar letouzey2010-11-02
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
* Numbers: NZPowProp as a Module Type, some module variable renamingGravatar letouzey2010-11-02
* Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etcGravatar letouzey2010-10-19
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Fix compilation by replacing some "auto with zarith" with "ring"Gravatar glondu2010-06-28
* Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).Gravatar herbelin2010-06-08
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* NMake: remove useless tactics abstract_pair, nicer commentsGravatar letouzey2010-03-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 03:08:51 +0000