Hi, I was looking at the migration for coq on Ubuntu and a build failure on armhf is preventing it.
I expect that this issue is fixed by the following commit: https://github.com/UniMath/UniMath/commit/1716c078b00c18dcabf63f671e414d7ba33cb23c Split the proof of associators_equiv to make sure it fits inside 32 b… …its (#1687) This is necessary to create a jscoq addon for UniMath (https://github.com/UniMath/UniMath-jsCoq). I haven't tried the patch yet and wanted to ask first if you're interested in restoring support for 32-bit arches. I honestly don't know if there's a lot of users on these (except maybe for JS). -- Adrien