aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Rational
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
2009-12-18RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndletouzey
2009-12-06Fix anomaly when using typeclass resolution with filtered hyps in evars.msozeau
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
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
2009-11-06Numbers: more (syntactic) changes toward new style of type classesletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
2008-07-04Fix bug #1899: no more strange notations for Qge and Qgtletouzey
2008-06-30QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...letouzey
2008-06-28QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...letouzey
2008-06-25Some work on BigQ :letouzey
2008-06-01BigQ: starting to create and use an interface QSigletouzey
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum pa...letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey