diff options
| -rw-r--r-- | src/Algebra/Ring.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index bf45155c8..acadec4df 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -92,7 +92,7 @@ Section Ring. forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)). Proof using Type*. intros; rewrite zero_product_iff_zero_factor; tauto. Qed. - Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq. + Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq := {}. Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops. Proof using Type*. split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances. |