diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/ZArithRing.v | 6 |
2 files changed, 2 insertions, 6 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 31372a0018..766473c6f6 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -835,7 +835,7 @@ destruct n. assert (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). - rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). + rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)%Z). simpl. rewrite Pcompare_refl. simpl. reflexivity. unfold Zminus, Zopp in H0. simpl in H0. rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 92a7539293..d3ed36ee9d 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -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 |