-
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
Add a pre_solve_closed ltac that basically changes the goal from `Closed X e` to `Closed ∅ e`. It is actually OK in practice.