aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/SpecViaZ/ZSig.v
AgeCommit message (Expand)Author
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2011-06-30Cleanup in SpecViaZletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2010-12-10First release of Vector library.pboutill
2010-12-09ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2letouzey
2010-12-06Numbers and bitwise functions.letouzey
2010-11-16Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.letouzey
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-11-02Numbers : log2. Abstraction, properties and implementations.letouzey
2010-10-19Add sqrt in Numbersletouzey
2010-10-14Numbers : also axiomatize constants 1 and 2.letouzey
2010-10-14Numbers: new functions pow, even, odd + many reorganisationsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-18More improvements of BigN, BigZ, BigQ:letouzey
2010-01-17BigN, BigZ, BigQ: presentation via unique module with both ops and propsletouzey
2010-01-08Numbers: BigN and BigZ get instantiations of all properties about div and modletouzey
2010-01-08Numbers: axiomatization + generic properties of abs and sgn.letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey