aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/SpecViaZ/NSig.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-07-01Cleanup of files related with power over Z.letouzey
2011-06-30Cleanup in SpecViaZletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2010-12-09ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2letouzey
2010-12-06Numbers and bitwise functions.letouzey
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-02-08DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationletouzey
2010-01-25NMake (and hence BigN): shiftr, shiftl now in the signature NSigletouzey
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
2009-11-10SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey