Hi, is `fix_undefined_universes`

(from 2015) still useful? It is used only for `Theorem`

and `Definition`

without body. Iiuc, it fixes (in the sense of blocking) the universe variables in the monomorphic mode so that they are not lowered to Set.

Are there examples that would break without it? At least, the test-suite passes.

Conversely, if needed for `Theorem`

and `Definition`

without body, it should be needed for all monomorphic cases with interactive proofs/obligations.

it is necessary for async proofs / vos I believe

Then, it should be added to all execution paths with proofs, right?

Last updated: Oct 13 2024 at 01:02 UTC