From d22a28998ef93a40eab673ea69034b1fc50247ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Jan 2017 11:08:49 +0100
Subject: [PATCH] lang/heap: do sealing with primitive projections

---
 opam.pins            |  2 +-
 theories/lang/heap.v | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/opam.pins b/opam.pins
index cbfb3aa0..dce32156 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq be81fb92a76f31ca656f8dad37122843f58884cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c83251df5e768aaa00e3f1f540fe668105b22712
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index a976118a..f27dbff4 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -43,10 +43,10 @@ Section definitions.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     heap_mapsto_st (RSt 0) l q v.
-  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
-  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
+  Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
+  Definition heap_mapsto := unseal heap_mapsto_aux.
   Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
-    proj2_sig heap_mapsto_aux.
+    seal_eq heap_mapsto_aux.
 
   Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
     ([∗ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
@@ -56,10 +56,10 @@ Section definitions.
 
   Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
     own heap_freeable_name (â—¯ {[ l.1 := (q, inter (l.2) n) ]}).
-  Definition heap_freeable_aux : { x | x = @heap_freeable_def }. by eexists. Qed.
-  Definition heap_freeable := proj1_sig heap_freeable_aux.
+  Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
+  Definition heap_freeable := unseal heap_freeable_aux.
   Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
-    proj2_sig heap_freeable_aux.
+    seal_eq heap_freeable_aux.
 
   Definition heap_inv : iProp Σ :=
     (∃ (σ:state) hF, ownP σ ∗ own heap_name (● to_heap σ)
-- 
GitLab