Benedikt Ahrens

A fix seems to be implemented here: https://github.com/coq/coq/pull/17697 The files to be installed are being written to a file instead of passed in a list.

If I understand https://github.com/coq/coq/pull/17697 correctly, specifically, this message "moved this from Request 8.18+rc1 inclusion to Shipped in 8.18+rc1 in [Coq 8.18](https://github.com/coq/coq/projects/57#card-89747440)" then the fix will be shipped in Coq 8.18,...

My `/bin/sh` points to "dash". But note that the Coq developers noticed this problem before us (specifically, the Coq Platform developers) and a fix has been prepared that will be...

It could be worth opening an issue with Coq, as soon as possible. Possibly this regression could be fixed before 8.20 is released.

This PR contains an axiom. I am thus converting it to a draft PR.

@rmatthes @Kfwullaert : do you have any feedback for this PR?

@DanGrayson : could you take a look?

@peterlefanulumsdaine : Thanks a lot for preparing this PR! > This PR demonstrates a crude alternative `#[local] Unset Universe Checking` in all files that need it, determined just by running...

Possibly stupidly simplistic idea: what if one replaces ``` Definition UU := Type. ``` with ``` Notation "'UU'" := Type. ``` or similar?

Possibly. However, we have the (long-term) goal of getting rid of type-in-type. Once this is achieved, we will need indices-matter.