Stream: MetaCoq

Topic: ✔ Notation clash with Int63


view this post on Zulip 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.
  1. Should I report a bug?
  2. In the meanwhile, is there a way to enjoy both libraries?
    Thanks!

view this post on Zulip Paolo Giarrusso (Jul 11 2021 at 15:01):

You can Require both but you cannot Import them both together, but only in different sections.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:12):

Indeed, that's a bug, should be easy to fix.

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:15):

https://github.com/MetaCoq/metacoq/pull/572

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:15):

@Chantal Keller Which MetaCoq version are you using btw?

view this post on Zulip Chantal Keller (Jul 12 2021 at 09:26):

Thanks! I am using the beta2 version.

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:28):

Good, it'll be in beta3

view this post on Zulip Notification Bot (Jul 12 2021 at 09:29):

Chantal Keller has marked this topic as resolved.

view this post on Zulip Notification Bot (Jul 12 2021 at 09:29):

Chantal Keller has marked this topic as resolved.

view this post on Zulip Notification Bot (Jul 12 2021 at 09:31):

Chantal Keller has marked this topic as unresolved.

view this post on Zulip Notification Bot (Jul 12 2021 at 09:55):

Matthieu Sozeau has marked this topic as resolved.

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 09:55):

It's now part of the 8.13 branch


Last updated: Mar 28 2024 at 10:01 UTC