Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
In Coq 8.6 type class search is not called recursively on premises that are not type classes. To that end, we use a hint extern to invoke an ordinary auto.
Robbert Krebbers authoredIn Coq 8.6 type class search is not called recursively on premises that are not type classes. To that end, we use a hint extern to invoke an ordinary auto.
