• Robbert Krebbers's avatar
    Fix issue #98. · e17ac4ad
    Robbert Krebbers authored
    We used to normalize the goal, and then checked whether it was of
    a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`,
    there was no way of making a distinction between the two, hence
    `True ⊢ P` was treated as `uPred_valid P`.
    In this commit, I use type classes to check whether the goal is of
    a certain shape. Since we declared `uPred_valid` as `Typeclasses
    Opaque`, we can now make a distinction between `True ⊢ P` and
    `uPred_valid P`.
proof.v 8.29 KB