• Robbert Krebbers's avatar
    Improve iExist. · 04e8c944
    Robbert Krebbers authored
    Now, it bases the type the quantifier ranges over on the goal, instead
    of the witness. This works better when dealing with witnesses involving
    type class constraints.
    04e8c944
tactics.v 39.5 KB