aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* Sorry for the mistake in r13702Gravatar pboutill2010-12-12
* 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
* Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,Gravatar herbelin2010-12-04
* 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
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
* 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
* NArith: a log2 functionGravatar 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
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
* Still another Open Scope than should be LocalGravatar letouzey2010-10-22
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
* Oups, new file Zsqrt_def was exporting Z_scopeGravatar letouzey2010-10-20
* 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
* Zeven: some complements, e.g. proofs that Zeven_bool and co are okGravatar letouzey2010-10-14
* NArith: add some functions Neven and NoddGravatar letouzey2010-10-14
* NArith: Definition of a Npow power functionGravatar letouzey2010-10-14
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
* Extraction: re-introduce some eta-expansions in rare situations leading to '_...Gravatar letouzey2010-09-20
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
* Minor fixes:Gravatar msozeau2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24