From 71efeff770db8d3576690d9eb5b598d50b52ab81 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Nov 2016 16:49:30 +0100
Subject: [PATCH] Fix compilation with current Iris.

---
 iris                |  2 +-
 theories/lifetime.v |  3 +--
 theories/perm.v     |  1 -
 theories/type.v     | 10 +++++++---
 4 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/iris b/iris
index 5e3835f8..8f33e282 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 5e3835f807768f42f77b6cc33bca039b8274a586
+Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 4d705fdb..193be22d 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -3,7 +3,6 @@ From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
 From iris.proofmode Require Import tactics.
 
 Definition lftN := nroot .@ "lft".
-
 Definition atomic_lft := positive.
 
 Definition lft_tokUR : ucmraT :=
@@ -185,7 +184,7 @@ Section lft.
   Lemma lft_own_static q : True ==∗ q.[static].
   Proof.
     rewrite /lft_own /static omap_empty fmap_empty.
-    apply (own_empty (A:=lft_tokUR) lft_toks_name).
+    apply (own_empty lft_tokUR lft_toks_name).
   Qed.
 
   Lemma lft_not_dead_static : [† static] ⊢ False.
diff --git a/theories/perm.v b/theories/perm.v
index ff983766..fbe763f4 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -91,7 +91,6 @@ Section duplicable.
 
 End duplicable.
 
-Hint Extern 0 (Is_true _.(ty_dup)) => exact I.
 
 Section has_type.
 
diff --git a/theories/type.v b/theories/type.v
index 348046e5..ebc124bc 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -22,7 +22,8 @@ Section type.
 Context `{iris_typeG Σ}.
 
 Record type :=
-  { ty_size : nat; ty_dup : bool;
+  { ty_size : nat;
+    ty_dup : bool;
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
 
@@ -108,6 +109,9 @@ Qed.
 
 End type.
 
+Hint Extern 0 (Is_true _.(ty_dup)) =>
+  exact I || assumption : typeclass_instances.
+
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
@@ -317,8 +321,8 @@ Section types.
     repeat setoid_rewrite tl_own_union; first last.
     set_solver. set_solver. set_solver. set_solver.
     iDestruct "Htl" as "[[Htl1 Htl2] $]".
-    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
-    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". done. set_solver.
+    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.
-- 
GitLab