The Coq mailing list

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

Hi, thx for filling the bug.

It is strange that this one did not happen before. It seems that
avoiding using "subst"  (and probably clear too) to remove section
variables that will use later is a workaround.

P.

2014-09-12 17:39 GMT+02:00 Eric Mullen 
<emullen AT cs.washington.edu>:
> After a good night of sleep I figured out what I did. Here is my minimal
> example which produces the error.
>
> Section FOO.
>
>   Variable x : nat.
>   Variable y : nat.
>   Hypothesis eq : x = y.
>
>   Lemma eq1 :
>     x = y.
>   Proof.
>     apply eq.
>   Qed.
>
>   Lemma eq2 :
>     x = y.
>   Proof.
>     subst.
>     rewrite <- eq1. (* produces the error *)
>
> I'll file a bug.
>
> Thanks,
> Eric
>
> On Fri, Sep 12, 2014 at 3:28 AM, Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
>>
>> 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
>>
>>
>