diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v index 41f23cb4e9e077c417ef1ea8ab0453fe98c19eeb..1bb7a7db18d1a9625bac28f2fbd313497c6396a3 100644 --- a/iris/base_logic/lib/gen_heap.v +++ b/iris/base_logic/lib/gen_heap.v @@ -188,10 +188,16 @@ Section gen_heap. Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed. (** Framing support *) + +Typeclasses Opaque mapsto. +Set Typeclasses Debug. +Set Typeclasses Debug Verbosity 2. + Global Instance frame_mapsto p l v q1 q2 q : FrameFractionalQp q1 q2 q → Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v) | 5. - Proof. apply: frame_fractional. Qed. + Proof. +Fail apply: frame_fractional. Qed. (** General properties of [meta] and [meta_token] *) Global Instance meta_token_timeless l N : Timeless (meta_token l N).