From 0a9eec4e28aea2ee601358aa2deb1d94af73a847 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 24 Jan 2019 01:05:14 +0100 Subject: Make trivial instances explicit This is in preparation for coq/coq#9274. --- src/Algebra/Ring.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Algebra') 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. -- cgit v1.2.3