aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/BigN/NMake.v
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Cleanup in SpecViaZGravatar 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
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
* 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
* NMake: remove useless tactics abstract_pair, nicer commentsGravatar letouzey2010-03-10
* NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...Gravatar letouzey2010-03-10
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation o...Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07