Stream: Coq devs & plugin devs

Topic: smtcoq conflicts with #17875

view this post on Zulip Hugo Herbelin (Aug 05 2023 at 16:14):

I don't know why this was not visible in the CI but there is apparently an incompatibility between smtcoq and #17875. I don't know if smtcoq developers are online these days. Somehow, it is smtcoq which should be changed: they should better not use Ppconstr.modular_constr_pr which is low-level. On the other side, they seem to really need what is called Ppconstr.pr_simpleconstr which is not exported. So maybe should we also export the latter at the Coq level...

Last updated: Dec 05 2023 at 12:01 UTC