• Robbert Krebbers's avatar
    Make iSpecialize work with coercions. · f1b30a2e
    Robbert Krebbers authored
    For example, when having `"H" : ∀ x : Z, P x`, using
    `iSpecialize ("H" $! (0:nat))` now works. We do this by first
    resolving the `IntoForall` type class, and then instantiating
    the quantifier.
    f1b30a2e
coq_tactics.v 33.7 KB