The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

I have never used tactic ring, but why using such a name while (nat, 0, +,
*) is not a ring?

> 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
>


-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay