Ana de Almeida Borges (Mar 04 2022 at 13:29): Ana de Almeida Borges (Mar 04 2022 at 13:29):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.
Pierre Roux (Mar 04 2022 at 13:39):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
Ana de Almeida Borges (Mar 04 2022 at 13:41):Cool, I didn't know that and it solves the problem, thanks!
Notification Bot (Mar 04 2022 at 13:41):Ana de Almeida Borges has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC