coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Local Fixpoints

From: Bernard Hurley<bernard AT marcade.biz>
To: coq-club AT inria.fr
Subject: [Coq-Club] Local Fixpoints
Date: Sat, 7 Apr 2012 02:36:55 +0200

Hi,

Is it possible to get the effect of a Local prefix with Fixpoint. I searched
the email archive but the solution I found (from 1999) doesn't work with the
current version of coq.

Thanks,

Bernard

[Coq-Club] Local Fixpoints, Bernard Hurley
- Re: [Coq-Club] Local Fixpoints, Tom Prince
  - Re: [Coq-Club] Local Fixpoints, Bernard Hurley