-
Robbert Krebbers authored
This way type class inference is not invokved when used in tactics like iPvs while not having to write an @. (Idea suggested by Ralf.)
de9438cb
This way type class inference is not invokved when used in tactics like iPvs while not having to write an @. (Idea suggested by Ralf.)