Stream: Coq devs & plugin devs

Topic: (Modules as namespaces) Shadowing between module aliases


view this post on Zulip Paolo Giarrusso (Oct 22 2023 at 04:09):

Re namespaces, I think I've seen scenarios where a constant was shadowed by an alias introduced by Include (might have been BinNat vs BinNatDef), which seems like unnecessary noise. At one point, my goal mentioned BinNat.foo and BinNatDef.bar, such that neither Import BinNat nor Import BinNatDef was a sufficient workaround (I didn't try selective imports). Would this warrant an issue, and need a minimization, or is this known?

I think Coq's smarter than this with abbreviations... How different should "user names" be from abbreviations over kernel names?

view this post on Zulip Hugo Herbelin (Oct 22 2023 at 11:21):

There is at least a known issue with Z.pos (here), but propbably not what you had in mind.


Last updated: Oct 13 2024 at 01:02 UTC