aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/BigZ/BigZ.v
AgeCommit message (Expand)Author
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-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-07-04Fix bug #1899: no more strange notations for Qge and Qgtletouzey
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey