coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive Function identifier "not found in the current environment"

From: julien.forest AT ensiie.fr
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Recursive Function identifier "not found in the current environment"
Date: Sat, 18 Oct 2014 10:28:50 +0200

On Sat, 18 Oct 2014 02:47:24 +0200
Christoph-Simon Senjak
<christoph.senjak AT ifi.lmu.de>
wrote:

Am 16.10.2014 um 18:23 schrieb
julien.forest AT ensiie.fr:
>
> On Thu, 16 Oct 2014 17:56:21 +0200
> Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:
>
>> buh je le vois pas le fix, il est caché?
>> P.
>>
>> 2014-10-16 17:46 GMT+02:00
<julien.forest AT ensiie.fr>:
>> >
>> > On Thu, 16 Oct 2014 15:53:01 +0200
>> > Christoph-Simon Senjak
<christoph.senjak AT ifi.lmu.de>
wrote:
>> >
>> >> Ok. Nevermind. There are pending obligations. I would have
>> >> expected that these are shown after the definition, just notice
>> >> that you have to ask for them.
>> >>
>> >> Am 15.10.2014 um 20:57 schrieb Christoph-Simon Senjak:
>> >> > Hello.
>> >> >
>> >> > I am using the current trunk
>> >> > (db8e0d7ecaf233ae73705d2f57635a38f8825dad). My overall project
>> >> > can be found under https://github.com/dasuxullebt/deflate/, I
>> >> > updated the file "InflateUnverified.v", I attached here.
>> >> >
>> >> > When I come to its last line, I get an error "The reference
>> >> > inflate was not found in the current environment". When I
>> >> > remove everything inside the "inflate" function, and only
>> >> > leave the (commented) catch-all pattern, it works.
>> >> >
>> >> > (Originally I wanted to do recursive extraction, which failed
>> >> > with the same error.)
>> >> >
>> >> > Best Regards
>> >> > Christoph-Simon Senjak
>> >>
>> >
>> > Hi Simon,
>> > your "inflate" function contains a "fix" construction which is
>> > not allowed by Function (See Section 2.3 of reference manual).
>> >
>> > Btw, I cannot reproduce the pending proof obligations. Can you
>> > tell me which version you are using ?
>> >
>> >
>> > Best regards,
>> >
>> > Julien Forest
>> >
>> >
> Dear Pierre,
> the fix construct is on line 194.
Line 194 is empty.
Regards, CSS

Hi Simon,
my answer was for the github version I got.

J.

[Coq-Club] Recursive Function identifier "not found in the current environment", Christoph-Simon Senjak, 10/15/2014
- Re: [Coq-Club] Recursive Function identifier "not found in the current environment", Christoph-Simon Senjak, 10/16/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Recursive Function identifier "not found in the current environment", julien . forest, 10/16/2014
  - Re: [Coq-Club] Recursive Function identifier "not found in the current environment", Pierre Courtieu, 10/16/2014
- Re: [Coq-Club] Recursive Function identifier "not found in the current environment", julien . forest, 10/16/2014
  - Re: [Coq-Club] Recursive Function identifier "not found in the current environment", Christoph-Simon Senjak, 10/18/2014
- Re: [Coq-Club] Recursive Function identifier "not found in the current environment", julien . forest, 10/18/2014
  - Re: [Coq-Club] Recursive Function identifier "not found in the current environment", Christoph-Simon Senjak, 10/18/2014