Stream: math-comp devs

Topic: ✔ Strange error with finmap


view this post on Zulip Julien Puydt (May 24 2022 at 12:24):

Excellent! That was it... thanks!

view this post on Zulip Notification Bot (May 24 2022 at 12:24):

Julien Puydt has marked this topic as resolved.

view this post on Zulip 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.)

view this post on Zulip Ana de Almeida Borges (May 24 2022 at 13:20):

Yeah, I have no idea and I also wonder.

view this post on Zulip 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: Aug 11 2022 at 02:03 UTC