summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/ZArithRing.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/setoid_ring/ZArithRing.v')
-rw-r--r--contrib/setoid_ring/ZArithRing.v16
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).
+