Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to make ring_nat available

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to make ring_nat available


chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
  • To: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
  • Cc: Jim Burton <jim AT sdf-eu.org>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] how to make ring_nat available
  • Date: Mon, 03 Nov 2008 09:44:27 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page