• Robbert Krebbers's avatar
    Fix possible divergence in framing. · ea791308
    Robbert Krebbers authored
    The instances frame_big_sepL_cons and frame_big_sepL_app could be
    applied repeatedly often when framing in [∗ list] k ↦ x ∈ ?e, Φ k x
    when ?e an evar. This commit fixes this bug.
    ea791308
classes.v 6.39 KB