The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

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