The Coq mailing list

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

Yves Bertot wrote:
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
The corrected version of "Coq in a Hurry" is now available at the 
following address:

http://cel.archives-ouvertes.fr/inria-00001173

However, I don't understand why the correction has not been propagated 
to arxiv.

Yves