-
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
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.