The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Adam,

If it makes sense to you, that doesn't mean it makes sense to everyone. This isn't the issue, however. I didn't say the manual doesn't make sense, but that maybe I was missing something that might be obvious to someone else with more experience in this matter.

I included an example with what didn't work for me in my reply to Stephane Glondu.


Thanks.

On Mon, Jun 27, 2011 at 13:56, Adam Chlipala <adam AT chlipala.net> wrote:

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.