• 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_collections.v 7.38 KB