From 157bee13827f9a616b6c82be4af110c8f2464c64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 May 2011 15:12:23 +0000
Subject: Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

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

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index ab63f7bf0e..6d0f40ac13 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -212,9 +212,9 @@ Proof.
       repeat rewrite <- eval_pol_norm ; simpl in *;
   unfold eval_expr;
   generalize (   eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs);
+    (fun x : N => x) (pow_N 1 Zmult) env lhs);
   generalize (eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
+    (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
   Transparent padd.
 Qed.
@@ -249,9 +249,9 @@ Proof.
       repeat rewrite <- eval_pol_norm ; simpl in *;
   unfold eval_expr;
   generalize (   eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs);
+    (fun x : N => x) (pow_N 1 Zmult) env lhs);
   generalize (eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
+    (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
   Transparent padd.
 Qed.
@@ -1009,7 +1009,7 @@ Definition eval := eval_formula.
 
 Definition prod_pos_nat := prod positive nat.
 
-Definition n_of_Z (z:Z) : BinNat.N :=
+Definition n_of_Z (z:Z) : N :=
   match z with
     | Z0 => N0
     | Zpos p => Npos p
-- 
cgit v1.2.3