After recompiling Debian packages to avoid "inconsistent assumptions" errors, I'm having issues with finmap: From mathcomp Require Import finmap.
triggers an error:
Error:
Level 2 is already declared right associative while it is now expected to be left associative.
and I have no clue what it means...
just doing From X Require Import Y.
in a file is not guaranteed to work, for any Coq project. It depends on what you have loaded previously
so I'm guessing this is some custom file that has Require-Imports above it?
It's a test of loading, so the file is only the line I gave.
Ah, From mathcomp.finmap Require Import multiset.
works.
So does From mathcomp.finmap Require Import set.
.
did you reproduce on pure opam installation? Works fine for me on coq-mathcomp-finmap.dev
I don't have opam.
This happens when you import finmap
without importing ssrfun
first. In general mathcomp stuff should only be imported after ssreflect ssrbool ssrfun
are imported.
Last updated: Aug 11 2022 at 02:03 UTC