• Jacques-Henri Jourdan's avatar
    Make iFrame able to accumulate assertions in an evar. · 09663be3
    Jacques-Henri Jourdan authored
    This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.
    09663be3
cancelable_invariants.v 3.87 KB