• 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
..
CG_stack.v Loading commit data...
FG_stack.v Loading commit data...
helping.v Loading commit data...
mailbox.v Loading commit data...
module_refinement.v Loading commit data...
refinement.v Loading commit data...
stack_rules.v Loading commit data...