• Robbert Krebbers's avatar
    Remove elem_of_tactic that uses intuition. · 4b4e270e
    Robbert Krebbers authored
    This one (previously solve_elem_of) was hardly used. The tactic that uses
    naive_solver (previously esolve_elem_of, now solve_elem_of) has been
    extended with flags to say which hypotheses should be cleared/kept.
    4b4e270e
fin_map_dom.v 6.06 KB