• 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
      ambiguity.
    a63f256e
fancy_updates.v 10.5 KB