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

Inductive cumulativity supports sort cumulativity (Prop <= Type)

c89fff8
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 error and 1 warning
Windows
failed Mar 24, 2026 in 34m 0s