Skip to content

Add Ltac2 Constr.strip_cast, head(_nocast) and decompose_app(_list)_nocast#22265

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

Add Ltac2 Constr.strip_cast, head(_nocast) and decompose_app(_list)_nocast#22265
JasonGross wants to merge 1 commit into
rocq-prover:masterfrom
JasonGross:ltac2-constr-nocast

Commits

Commits on Jul 16, 2026