1 files changed, 35 insertions, 12 deletions
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4f47fff0..8de7021e 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -8,26 +8,49 @@
 
 Require Export Ring.
 Require Import ZArith_base.
+Require Import Zpow_def.
+
 Import InitialRing.
 
 Set Implicit Arguments.
 
-Ltac isZcst t :=
-  let t := eval hnf in t in
-  match t with
-    Z0 => constr:true
-  | Zpos ?p => isZcst p
-  | Zneg ?p => isZcst p
-  | xI ?p => isZcst p
-  | xO ?p => isZcst p
-  | xH => constr:true
-  | _ => constr:false
-  end.
 Ltac Zcst t :=
   match isZcst t with
     true => t
   | _ => NotConstant
   end.
 
+Ltac isZpow_coef t :=
+  match t with 
+  | Zpos ?p => isPcst p
+  | Z0 => true
+  | _ => false
+  end.
+
+Definition N_of_Z x :=
+ match x with
+ | Zpos p => Npos p
+ | _ => N0
+ end.
+
+Ltac Zpow_tac t :=
+ match isZpow_coef t with
+ | true => constr:(N_of_Z t)
+ | _ => constr:(NotConstant)
+ end.
+
+Ltac Zpower_neg :=
+  repeat match goal with
+  | [|- ?G] => 
+    match G with 
+    | context c [Zpower _ (Zneg _)] =>
+      let t := context c [Z0] in
+      change t
+    end
+  end.   
+
+
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]).
+  (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+   power_tac Zpower_theory [Zpow_tac]).
+