diff options
Diffstat (limited to 'contrib/ring/Ring_theory.v')
| -rw-r--r-- | contrib/ring/Ring_theory.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 2901942ef..c04eee57e 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -370,6 +370,8 @@ Save. End Theory_of_rings. +Hints Resolve Th_mult_zero_left Th_plus_reg_left : core. + Implicit Arguments Off. Definition Semi_Ring_Theory_of : |