Skip to content

Inductive cumulativity supports sort cumulativity (Prop <= Type)#21773

Closed
SkySkimmer wants to merge 1 commit into
rocq-prover:masterfrom
SkySkimmer:cumul-sort-poly
Closed

Inductive cumulativity supports sort cumulativity (Prop <= Type)#21773
SkySkimmer wants to merge 1 commit into
rocq-prover:masterfrom
SkySkimmer:cumul-sort-poly

Commits

Commits on Mar 24, 2026