Forked from
Iris / Iris
Source project has a limited visibility.
-
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.)
Robbert Krebbers authoredThis way type class inference is not invokved when used in tactics like iPvs while not having to write an @. (Idea suggested by Ralf.)
