• 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
Name
Last commit
Last update
..
stack Loading commit data...
bit.v Loading commit data...
counter.v Loading commit data...
generative.v Loading commit data...
lateearlychoice.v Loading commit data...
lock.v Loading commit data...
or.v Loading commit data...
par.v Loading commit data...
symbol.v Loading commit data...
ticket_lock.v Loading commit data...
various.v Loading commit data...