• Dan Frumin's avatar
    More robust solve_closed tactic · 59d1cab3
    Dan Frumin authored
    Add a pre_solve_closed ltac that basically changes the goal from
    `Closed X e` to `Closed ∅ e`. It is actually OK in practice.
    59d1cab3
helping.v 21.9 KB