Skip to content

Add Ltac2 Constr.is_prop, is_set, is_sprop, is_type and is_type_or_set#22264

Draft
JasonGross wants to merge 1 commit into
rocq-prover:masterfrom
JasonGross:ltac2-constr-sort-predicates
Draft

Add Ltac2 Constr.is_prop, is_set, is_sprop, is_type and is_type_or_set#22264
JasonGross wants to merge 1 commit into
rocq-prover:masterfrom
JasonGross:ltac2-constr-sort-predicates

Commits

Commits on Jul 11, 2026