Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
The PR redirects all UState.restrict in declare.ml towards a reusable encapsulation make_univs of the three functions used to build deferred, private or regular universe restriction.
The impact is modest at this stage as it only ensures that Set Private Universes is used when defining an opaque non-interactive fixpoints (so assuming that a sealed attribute is available). To go towards more factorisation, we would need to modify Evarutil.finalize which is the other execution path used to restrict universes (finalize do minimization, evar check, restriction but not universe declaration check, while make_univs makes restriction and universe declaration check). See coq/ceps#89 for discussions.
The PR redirects all
UState.restrictindeclare.mltowards a reusable encapsulationmake_univsof the three functions used to build deferred, private or regular universe restriction.The impact is modest at this stage as it only ensures that
Set Private Universesis used when defining an opaque non-interactive fixpoints (so assuming that asealedattribute is available). To go towards more factorisation, we would need to modifyEvarutil.finalizewhich is the other execution path used to restrict universes (finalizedo minimization, evar check, restriction but not universe declaration check, whilemake_univsmakes restriction and universe declaration check). See coq/ceps#89 for discussions.Depends on:
18743
18795.