Merge branch 'experimental/upstream' into upstream

1 files changed, 4 insertions, 8 deletions

diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 362542b9..3c4f6b86 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -27,11 +27,7 @@ Ltac isZpow_coef t :=
   | _ => constr:false
   end.
 
-Definition N_of_Z x :=
- match x with
- | Zpos p => Npos p
- | _ => N0
- end.
+Notation N_of_Z := Z.to_N (only parsing).
 
 Ltac Zpow_tac t :=
  match isZpow_coef t with
@@ -43,14 +39,14 @@ Ltac Zpower_neg :=
   repeat match goal with
   | [|- ?G] =>
     match G with
-    | context c [Zpower _ (Zneg _)] =>
+    | context c [Z.pow _ (Zneg _)] =>
       let t := context c [Z0] in
       change t
     end
   end.
 
 Add Ring Zr : Zth
-  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of
         coefficiant is usual ring Z *)