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: Jul 13 2024 at 03:01 UTC