• Robbert Krebbers's avatar
    Rewrite set_unfold using type classes. · 9201446c
    Robbert Krebbers authored
    It now traverses terms at most once, whereas the setoid_rewrite
    approach was travering terms many times. Also, the tactic can now
    be extended by defining type class instances.
    9201446c
sets.v 2.2 KB