Skip to content

Fix Tactics.descend_in_conjunctions on inductives with letins in constructors#21063

Merged
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:fix-apply-nreal
Sep 22, 2025
Merged

Fix Tactics.descend_in_conjunctions on inductives with letins in constructors#21063
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:fix-apply-nreal

Commits

Commits on Sep 5, 2025