The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have a script find-bug.py at https://github.com/JasonGross/coq-bug-finder that can probably automatically create a standalone example for you; you give it a file in the middle of a development that, when compiled, gives the anomaly, and it will hand you back a stand-alone file giving the same anomaly.

-Jason

On Fri, Sep 12, 2014 at 5:28 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi,

The message clearly states that it is a bug: even if you did something
wrong the message itself is wrong. For some reason the variable is not
in the environment anymore (maybe you closed the section?) but
something asked for it.

Please try to provide a standalone file producing the error, otherwise
we cannot help you.

You should file a bug report in the coq bug tracking system
(https://coq.inria.fr/bugs/) and attach the file.

You may post the file here anyway so that we help you out of this.

Best regards,
Pierre

2014-09-12 9:51 GMT+02:00 Eric Mullen <emullen AT cs.washington.edu>:
> I got the this error message while working on a large project (an extension
> to compcert). What does it mean?
>
> Toplevel input, characters 0-35:
> Anomaly: type_of: variable tprog unbound. Please report.
>
> The variable tprog is a section variable defined earlier in the file.
>
> I have a screenshot of the error as well (not attached, but feel free to
> email me for it). I have a git commit of the exact state of the code where
> the error occurred, and I have the emacs/coqtop instance still running (if
> there's a way to get more debug information out).
>
> I'm using Coq 8.4pl3, ProofGeneral version 4.2, Emacs version 24.3.1
>
> Thanks,
> Eric