Chantal Keller (Jul 11 2021 at 11:56): Chantal Keller (Jul 11 2021 at 11:56):Hi
There is a notation clash between MetaCoq (PCUICEquality) and Int63:
Require Import Int63.
Require Import MetaCoq.PCUIC.PCUICEquality.
fails with
Error: Notation "_ ≡ _" is already defined at level 70 with arguments constr at next level, constr at next level while it is now required to be at level 60 with arguments constr at next level, constr at next level.
You can Require both but you cannot Import them both together, but only in different sections.
Paolo Giarrusso (Jul 11 2021 at 15:02):I'd say that's a bug and the right priority is 70, like the one of equality — IIRC, Int63 was fixed to use 70, so MetaCoqshould follow suit
Matthieu Sozeau (Jul 12 2021 at 09:12):Indeed, that's a bug, should be easy to fix.
Matthieu Sozeau (Jul 12 2021 at 09:15):https://github.com/MetaCoq/metacoq/pull/572
Matthieu Sozeau (Jul 12 2021 at 09:15):@Chantal Keller Which MetaCoq version are you using btw?
Chantal Keller (Jul 12 2021 at 09:26):Thanks! I am using the beta2 version.
Matthieu Sozeau (Jul 12 2021 at 09:28):Good, it'll be in beta3
Notification Bot (Jul 12 2021 at 09:29):Chantal Keller has marked this topic as resolved.
Notification Bot (Jul 12 2021 at 09:29):Chantal Keller has marked this topic as resolved.
Notification Bot (Jul 12 2021 at 09:31):Chantal Keller has marked this topic as unresolved.
Notification Bot (Jul 12 2021 at 09:55):Matthieu Sozeau has marked this topic as resolved.
Matthieu Sozeau (Jul 12 2021 at 09:55):It's now part of the 8.13 branch
Last updated: May 31 2023 at 04:01 UTC