diff options
author | 2010-01-18 17:53:15 +0000 | |
---|---|---|
committer | 2010-01-18 17:53:15 +0000 | |
commit | d3db79fcd7c06c62c08120d43176fbb36124770f (patch) | |
tree | ad21ef98ed36a26b8c7cb2be6e0c8644ef70df85 /Makefile.doc | |
parent | cd4f47d6aa9654b163a2494e462aa43001b55fda (diff) |
More improvements of BigN, BigZ, BigQ:
- ring/field: detection of constants for ring/field,
detection of power, potential use of euclidean division.
- for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
- mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
By the way, BigN.zify could still be improved (no insertion of positivity
hyps yet, unlike the original zify).
- debug of BigQ.qify (autorewrite was looping on spec_0).
- for BigQ, start of a generic functor of properties QProperties.
- BigQ now implements OrderedType, TotalOrder, and contains facts
about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions