1 files changed, 10 insertions, 6 deletions
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 8de7021e..4a5b623b 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
 Ltac Zcst t :=
   match isZcst t with
     true => t
-  | _ => NotConstant
+  | _ => constr:NotConstant
   end.
 
 Ltac isZpow_coef t :=
   match t with 
   | Zpos ?p => isPcst p
-  | Z0 => true
-  | _ => false
+  | Z0 => constr:true
+  | _ => constr:false
   end.
 
 Definition N_of_Z x :=
@@ -36,7 +36,7 @@ Definition N_of_Z x :=
 Ltac Zpow_tac t :=
  match isZpow_coef t with
  | true => constr:(N_of_Z t)
- | _ => constr:(NotConstant)
+ | _ => constr:NotConstant
  end.
 
 Ltac Zpower_neg :=
@@ -49,8 +49,12 @@ Ltac Zpower_neg :=
     end
   end.   
 
-
 Add Ring Zr : Zth
   (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
-   power_tac Zpower_theory [Zpow_tac]).
+   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 *)
+    div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)),
+   sign get_signZ_th).
+