The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Lucian M. Patcas wrote:
> I need to define a ring structure and convince the ring tactic to use 
> it. I looked in the manual and in the module Ring_theory. I also 
> looked at how nat is "registered" as a ring in 
> Coq.setoid_ring.ArithRing, but I still don't know how exactly to 
> define a ring structure and how to use Add Ring. Perhaps I'm missing 
> something. Can someone help out?

Perhaps you could tell us which is the first bit of Section 23.5 of the 
Coq manual that doesn't make sense to you?  I've found it to be a 
reasonable guide to the use of the ring tactics.