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?
This seems indeed like a bug (present since version 8.5). Thanks for reporting!
Can I make a issue about that?
Last updated: Oct 13 2024 at 01:02 UTC