• Robbert Krebbers's avatar
    Make iDestruct smarter about when to copy a hypothesis. · fdfc790d
    Robbert Krebbers authored
    It now copies the hypothesis when: 1.) it is persistent 2.) when destructing
    it requires a universal quantifier to be instantiated. The new behavior is
    implemented using a type class (called CopyDestruct) so that it can easily be
    extended.
    fdfc790d
tactics.v 60.5 KB