A common execution path for universe restriction + universe declaration check - #19031

Merged

coqbot-app[bot] merged 3 commits into

rocq-prover:masterfrom

herbelin:master+factorization-make-univs-declare.ml

Sep 5, 2024

Commits on Jul 26, 2024

Declare.ml: centralize the management of universes.
herbelin
committed
3658411
Attach an UState.t to each individual entry of a block of entries (for use in hooks).
herbelin
committed
04cdc8e
Take "Set Private Universes" into account in opaque non-interactive definitions and fixpoints.
herbelin
committed
832aeb9