Skip to content

add odestruct and other "open term" tactics

Ralf Jung requested to merge ralf/odestruct into master

See the added testcase for motivation. Every now and then I run into the situation where I need a tactic like this and then not having it is always super frustrating...

Thanks a lot to @janno for help in writing these tactics!

Edited by Ralf Jung

Merge request reports