abstract tactic doesn't work when the top-level proof is sort-polymorphic #19072
Labels
kind: bug
An error, flaw, fault or unintended behaviour.
part: sort polymorphism
The sorts subsystem of the universe system.
Milestone
Description of the problem
Version of Coq where this bug occurs
8.19.0
Last version of Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered: