-
Robbert Krebbers authored
There is no need to restrict the type class using Hint Mode, we have a default instance that will always be used first. In case of evars, the default instance should apply. The reason for this change is that `iAssumption` should be able to prove `H : ?e |- P` and `H : P |- ?e`. The former Hint Mode prevented it from doing that.
2cbcc992