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?
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