coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] variable not found in the current environment

From: Keiko Nakata <(e6fa90e88c%hidden_head%e6fa90e88c)keiko(e6fa90e88c%hidden_at%e6fa90e88c)kurims.kyoto-u.ac.jp(e6fa90e88c%hidden_end%e6fa90e88c)>
To: (e6fa90e88c%hidden_head%e6fa90e88c)coq-club(e6fa90e88c%hidden_at%e6fa90e88c)pauillac.inria.fr(e6fa90e88c%hidden_end%e6fa90e88c)
Subject: [Coq-Club] variable not found in the current environment
Date: Wed, 16 Dec 2009 23:19:58 +0900 (JST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

Trying to define a function with the Program command,
I got an error

The variable s0' was not found in the current environment.

But my code does not contain any occurrence of s0'.
What would be my problem?

I am not sure if this is relevant,
but I am defining a corecursive function, i.e. Program CoFixpoint.

Best,
Keiko

[Coq-Club] variable not found in the current environment, Keiko Nakata
- Re: [Coq-Club] variable not found in the current environment, AUGER