Forked from
Iris / Iris
5855 commits behind the upstream repository.
-
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.
