Hugo Herbelin (Aug 05 2023 at 16:14): 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