aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-08 09:54:31 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-08 09:54:31 +0000
commitc08b8247aec05b34a908663aa160fdbd617b8220 (patch)
tree58bf890038871e9538cbc0d4be66374571adbaed /library/libnames.mli
parent9a57002cd644bac29e0ad338756d1a01613e6c13 (diff)
setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.
A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.mli')
0 files changed, 0 insertions, 0 deletions