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.
Excellent! That was it... thanks!
Julien Puydt has marked this topic as resolved.
(Though I still wonder why @Karl Palmskog didn't see it, and I wonder if finmap hence shouldn't import what it needs beforehand.)
Yeah, I have no idea and I also wonder.
I tried in both ProofGeneral/Emacs and
coqc with the
dev/repo version of finmap. Maybe someone wants to try a naked
From mathcomp Require Import finmap. on Nix. Or maybe only finmap 1.5.1 and below has this behavior? The release is about 1.5 years old at this point.
Last updated: May 31 2023 at 03:30 UTC