From d2f8b6897555c9a3fbe21111dc68519ec63e5773 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 23 Apr 2019 22:56:16 +0200
Subject: [PATCH] Make use of new `SetUnfoldElemOf`.

---
 theories/heap_lang/lang.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 3cf55913b..78a2aa862 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -52,9 +52,9 @@ Instance binder_eq_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
 
 Instance set_unfold_cons_binder x mx X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
+  SetUnfoldElemOf x X P → SetUnfoldElemOf x (mx :b: X) (BNamed x = mx ∨ P).
 Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
+  constructor. rewrite -(set_unfold_elem_of x X P).
   destruct mx; rewrite /= ?elem_of_cons; naive_solver.
 Qed.
 
-- 
GitLab