GitLab

In !739 (merged) we have removed the general frame_fractional instance and replaced it by connection-specific framing instances such as:

  Global Instance frame_mapsto p l v q1 q2 RES :
    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.

This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than frame_fractional.

However, we have more Fractional instances in the codebase, which for now do not support framing any more:

• Fractional (λ q, mono_nat_auth_own γ q n)
• Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)
• Fractional (λ q, k ↪[γ]{#q} v) (for ghost_map)
• Fractional (λ q, ghost_map_auth γ q m)
• Fractional (λ q, ghost_var γ q a)
• Fractional (cinv_own γ)

If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.