From d2bd5d87d23d443f6e41496bdfe5f8e82d675634 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 May 2011 15:12:59 +0000
Subject: Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/ZMicromega.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 6d0f40ac13..2db4db6765 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -1009,12 +1009,7 @@ Definition eval := eval_formula.
 
 Definition prod_pos_nat := prod positive nat.
 
-Definition n_of_Z (z:Z) : N :=
-  match z with
-    | Z0 => N0
-    | Zpos p => Npos p
-    | Zneg p => N0
-  end.
+Notation n_of_Z := Z.to_N (only parsing).
 
 (* Local Variables: *)
 (* coding: utf-8 *)
-- 
cgit v1.2.3