Stream: Coq devs & plugin devs

Topic: Fixing bug #17833


view this post on Zulip Jason Gross (Jul 27 2023 at 22:01):

I'm interested in porting a project I'm working on from 8.17 to master, in part because I want to try out a fix for #17893 (primitive float fma) on it. Currently blocked by #17833, about the "Missing notation term for variables" error regression. I don't understand @Gaëtan Gilbert 's suggestion well enough to implement the fix myself, but if it's not too complicated, I'd be interested in giving it a shot with a bit more guidance. (Alternatively, I'd be quite happy if one of the other devs (@Gaëtan Gilbert ? @Hugo Herbelin ?) had a(n easy) fix for at least the regression part of the issue.)

view this post on Zulip Gaëtan Gilbert (Jul 27 2023 at 22:07):

I'll look at it next week
I'm on holidays this week so I'm not doing any serious work

view this post on Zulip Jason Gross (Jul 27 2023 at 22:13):

Thank you!


Last updated: Dec 05 2023 at 12:01 UTC