aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Update headers.Gravatar Maxime Dénès2015-01-12
* eta contractionsGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* More dynamic argument scopesGravatar letouzey2013-07-17
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Updating headers.Gravatar herbelin2012-08-08
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Cleanup of NdigitsGravatar letouzey2011-06-30
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* BinNat: N.binary_rect is now a definition instead of an opaque proofGravatar letouzey2011-05-05
* Peano recursion for positive: integration of Daniel Schepler's codeGravatar letouzey2011-05-05
* Minimal lemmas about Z.gt, N.gt and coGravatar 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
* Modularization of NnatGravatar 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
* 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
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Vectors fully use implicit argumentsGravatar pboutill2011-02-10
* 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
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* 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
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* NArith: a log2 functionGravatar letouzey2010-11-02
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Still another Open Scope than should be LocalGravatar letouzey2010-10-22