Is there anything that can be done about managing different scopes with the same key? For example,
%Z is the delimiting key for both the stdlib integers and the mathcomp integers. I'm thinking something like
%ZArith.Z to be more specific, although that of course does not work.
I don't think so, but one can always reasign keys. In validsdp, we have that for instance: https://github.com/validsdp/validsdp/blob/master/theories/cholesky_prog.v#L25
Cool, I didn't know that and it solves the problem, thanks!
Ana de Almeida Borges has marked this topic as resolved.
Last updated: Sep 23 2023 at 14:01 UTC