rocq-prover

Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed.

The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments.

The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport.

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint.

Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type.