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...
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.
From mathcomp.finmap Require Import multiset. works.
From mathcomp.finmap Require Import set..
did you reproduce on pure opam installation? Works fine for me on
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