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: Feb 09 2023 at 02:02 UTC