From a5e0c0194b57742e00c16a4a59eed2a4604dcd54 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 May 2018 17:00:24 +0200
Subject: [PATCH] port some small tweak from gen_proofmode

---
 opam                    | 2 +-
 theories/lang/heap.v    | 6 +++---
 theories/lang/tactics.v | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/opam b/opam
index 8b3aee44..2d74ba79 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-05-23.0.4fc7ee79") | (= "dev") }
+  "coq-iris" { (= "dev.2018-05-23.1.b043f3a3") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index d2bde800..fd04e13d 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -141,7 +141,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 uPred.discrete_valid.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
     rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
@@ -461,7 +461,7 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
         ∗ heap_mapsto_st (RSt n2) l q v.
   Proof.
-    intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
@@ -510,7 +510,7 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
         ∗ heap_mapsto_st st2 l 1%Qp v'.
   Proof.
-    intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply exclusive_local_update. by destruct st2.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 31301b9d..f37ad06d 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -120,7 +120,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
   | Val v e H => Val v e H
-  | @ClosedExpr e H => @ClosedExpr e H
+  | ClosedExpr e => ClosedExpr e
   | Var y => if bool_decide (y = x) then es else Var y
   | Lit l => Lit l
   | Rec f xl e =>
-- 
GitLab