The Coq mailing list

[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