heap tuning

algebra/cmra.v

@@ -338,6 +338,9 @@ Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
 Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
 Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
 
+Global Instance local_update_id : LocalUpdate (λ _, True) (@id A).
+Proof. split; auto with typeclass_instances. Qed.
+
 (** ** Updates *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.

heap_lang/heap.v

@@ -44,7 +44,7 @@ Section heap.
   Definition heap_ctx (γ : gname) : iPropG heap_lang Σ :=
     auth_ctx HeapI γ N heap_inv.
 
-  Global Instance heap_inv_ne : Proper ((≡) ==> (≡)) heap_inv.
+  Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
   Proof.
     move=>? ? EQ. rewrite /heap_inv /from_heap.
     (* TODO I guess we need some lemma about omap? *)
@@ -91,8 +91,8 @@ Section heap.
     apply later_mono, wand_intro_l. rewrite left_id const_equiv // left_id.
     by rewrite -later_intro.
   Unshelve.
+  (* TODO Make it so that this becomes a goal, not shelved. *)
   { eexists. eauto. }
-  { split; first by apply _. done. }
   Qed.
 
 End heap.