diff options
| author | letouzey | 2007-11-08 09:54:31 +0000 |
|---|---|---|
| committer | letouzey | 2007-11-08 09:54:31 +0000 |
| commit | c08b8247aec05b34a908663aa160fdbd617b8220 (patch) | |
| tree | 58bf890038871e9538cbc0d4be66374571adbaed /Makefile.common | |
| parent | 9a57002cd644bac29e0ad338756d1a01613e6c13 (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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 8e3294ee62..a28b456b98 100644 --- a/Makefile.common +++ b/Makefile.common @@ -509,7 +509,8 @@ ZARITHVO:=\ theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo \ - theories/ZArith/Zpow_def.vo theories/ZArith/Zpow_facts.vo + theories/ZArith/Zpow_def.vo theories/ZArith/Zpow_facts.vo \ + theories/ZArith/ZOdiv_def.vo theories/ZArith/ZOdiv.vo INTSVO:=\ theories/Ints/Z/ZAux.vo \ @@ -734,7 +735,7 @@ NEWRINGVO:=\ contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo \ contrib/setoid_ring/Ring_equiv.vo contrib/setoid_ring/Ring.vo \ contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/NArithRing.vo \ - contrib/setoid_ring/ZArithRing.vo contrib/setoid_ring/Ring_zdiv.vo \ + contrib/setoid_ring/ZArithRing.vo \ contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo \ contrib/setoid_ring/Field.vo contrib/setoid_ring/RealField.vo |