From 3c32ead9ea59348c0b85b2e2d89b114f540145c4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Dec 2016 20:07:35 +0100
Subject: [PATCH] Fix build (change of names).

---
 theories/lang/heap.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index b0e3d4b1..86fb2d25 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -144,7 +144,7 @@ Section heap.
   Lemma heap_mapsto_agree l q1 q2 v1 v2 :
     l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
     rewrite op_singleton pair_op singleton_valid. case.
     rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto.
-- 
GitLab