theories/proofmode/class_instances.v · ea7913081b7554d4d8191c0cfe99bfd736d22343 · Simcha van Collem / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Fix possible divergence in framing. · ea791308

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

History

Fix possible divergence in framing.

Robbert Krebbers authored 8 years ago

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.