The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Jim Burton wrote:
> Hi, I'm a beginner working through "Coq In a Hurry". In the section on proof
> by induction ring_nat is used but I get:
>
> Error: The reference ring_nat was not found in the current environment
>
> I have tried importing various likely sounding packages to no avail -- which
> do I need? More importantly, how to find this information myself next time?
>
> Many thanks,
>
> Jim Burton
>   
Hello,

My mistake is that I never corrected that tutorial on the web-site: 
ring_nat is not
the right name for the tactic: ring will to the trick.

I have a correct version of coq-in-a-hurry on my computer, and I will try to
update all the pointers under my responsibility as soon as possible.

Yves