• Robbert Krebbers's avatar
    Special proof mode class for adding a modality to a goal. · a63f256e
    Robbert Krebbers authored
    This used to be done by using `ElimModal` in backwards direction. Having
    a separate type class for this gets rid of some hacks:
    - Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
    - Weird type class precedence hacks to make sure the right instance is picked.
      These were needed because using `ElimModal` in backwards direction caused
classes.v 12.8 KB