Stream: Coq devs & plugin devs

Topic: Some strange about glob of references


view this post on Zulip YOSHIHIRO Imai (Aug 30 2024 at 07:54):

I looked at the glob file of a Coq code using local modules and found something a little odd.

For example, take a look at the glob file created by compiling the following source code:

Module Mod.
  Definition x := tt.
End Mod.
Check Mod.x.

The generated glob file is as follows:

DIGEST 3d2a81e525665a7e56f45fb24b500174
FHoge
mod 7:9 <> Mod
def 25:25 Mod x
R30:31 Coq.Init.Datatypes <> tt constr
R38:40 Hoge Mod <> mod
R49:53 Hoge <> x def

The reference to x in the last line of this glob does not include the module name Mod. Is this the expected behavior?

view this post on Zulip Hugo Herbelin (Aug 30 2024 at 09:10):

This seems indeed like a bug (present since version 8.5). Thanks for reporting!

view this post on Zulip YOSHIHIRO Imai (Aug 30 2024 at 09:13):

Can I make a issue about that?


Last updated: Oct 13 2024 at 01:02 UTC