From 2f2a1e346f467d4a8d21c6cfa4047c1b12a7851b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Mar 2017 12:37:17 +0100
Subject: [PATCH] Bump Iris.

---
 opam.pins                           | 2 +-
 theories/lang/heap.v                | 6 ++----
 theories/lifetime/model/primitive.v | 7 ++++---
 3 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/opam.pins b/opam.pins
index 4e9b917a..b0471b4c 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4a154f085ab5be64d30eec3967f1ab46b5467061
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index f3f69a16..1bc07739 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -139,13 +139,11 @@ Section heap.
   Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
 
-  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  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 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.
+    rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
 
   Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1d640781..44909254 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -58,6 +58,7 @@ Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
 Qed.
+
 Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
 Proof.
   iSplit.
@@ -65,7 +66,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
@@ -99,7 +100,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
@@ -133,7 +134,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
-- 
GitLab