• Robbert Krebbers's avatar
    Change Hint Mode for FromAssumption. · 2cbcc992
    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
class_instances.v 31.3 KB