The Coq mailing list

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

Regards,
Julien