diff options
| author |  Maxime Dénès <maxime.denes@inria.fr> | 2019-01-24 01:05:14 +0100 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-24 11:36:17 -0500 |
| commit | 0a9eec4e28aea2ee601358aa2deb1d94af73a847 (patch) | |
| tree | 7e3b89c5c7012b9edafb21bfedfff74a2f1be74d /src/Algebra | |
| parent | 226c05f2db7177cd33fffef6546d0385d6a1492f (diff) | |
Make trivial instances explicit
This is in preparation for coq/coq#9274.
Diffstat (limited to 'src/Algebra')
| -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. |