Julien Puydt (May 24 2022 at 12:24): Julien Puydt (May 24 2022 at 12:24):Excellent! That was it... thanks!
Notification Bot (May 24 2022 at 12:24):Julien Puydt has marked this topic as resolved.
Julien Puydt (May 24 2022 at 12:59):(Though I still wonder why @Karl Palmskog didn't see it, and I wonder if finmap hence shouldn't import what it needs beforehand.)
Ana de Almeida Borges (May 24 2022 at 13:20):Yeah, I have no idea and I also wonder.
Karl Palmskog (May 24 2022 at 13:31):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