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

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 4e8373f60..9b0c88669 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1125,8 +1125,8 @@ Definition Zabs_N (z:Z) :=
     | Zneg p => Npos p
   end.
 
-Definition Z_of_N (x:N) := match x with
-                             | N0 => Z0
-                             | Npos p => Zpos p
-                           end.
-
+Definition Z_of_N (x:N) := 
+  match x with
+    | N0 => Z0
+    | Npos p => Zpos p
+  end.