The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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