aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Int31/Int31.v
AgeCommit message (Expand)Author
2010-01-19Ring31 : a ring structure and tactic for int31letouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-02newton iteration for sqrt31thery
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-05-26Int31 : gcd31 was wrongletouzey
2008-05-23(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...letouzey
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good id...letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
2008-05-16More BigNum cleanup: letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 16:52:58 +0000