• 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
..
F_mu_ref_conc Loading commit data...
examples Loading commit data...
logrel Loading commit data...
prelude Loading commit data...
tests Loading commit data...
logrel.v Loading commit data...