From f7c8b3a36db61b3149c57f747ffc78ee42f3442f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Feb 2019 16:01:45 +0100
Subject: [PATCH] Bump Iris, make compatible with Coq master.

---
 opam                          | 2 +-
 theories/algebra/vfrac_auth.v | 4 ++--
 theories/bi/fracpred.v        | 2 +-
 theories/iron_logic/fcinv.v   | 2 +-
 theories/iron_logic/iron.v    | 4 ++--
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/opam b/opam
index 295486e..3c841a3 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
 depends: [
-  "coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
+  "coq-iris" { (= "dev.2019-02-01.0.de7eab03") | (= "dev") }
 ]
 
diff --git a/theories/algebra/vfrac_auth.v b/theories/algebra/vfrac_auth.v
index 6a4ff89..32dc765 100644
--- a/theories/algebra/vfrac_auth.v
+++ b/theories/algebra/vfrac_auth.v
@@ -35,8 +35,8 @@ Definition vfrac_auth_frag {A : cmraT} (q : Qp) (x : A) : vfrac_authR A :=
 
 Typeclasses Opaque vfrac_auth_auth vfrac_auth_frag.
 
-Instance: Params (@vfrac_auth_auth) 2.
-Instance: Params (@vfrac_auth_frag) 2.
+Instance: Params (@vfrac_auth_auth) 2 := {}.
+Instance: Params (@vfrac_auth_frag) 2 := {}.
 
 Notation "●?{ q } a" := (vfrac_auth_auth q a) (at level 10, format "●?{ q }  a").
 Notation "◯?{ q } a" := (vfrac_auth_frag q a) (at level 10, format "◯?{ q }  a").
diff --git a/theories/bi/fracpred.v b/theories/bi/fracpred.v
index 092f262..5cff46f 100644
--- a/theories/bi/fracpred.v
+++ b/theories/bi/fracpred.v
@@ -269,7 +269,7 @@ Class FObjective {PROP : bi} (P : fracPred PROP) :=
 Arguments FObjective {_} _%I.
 Arguments fobjective_at {_} _%I {_}.
 Hint Mode FObjective + ! : typeclass_instances.
-Instance: Params (@FObjective) 1.
+Instance: Params (@FObjective) 1 := {}.
 
 (** Primitive facts that cannot be deduced from the BI structure. *)
 Section bi_facts.
diff --git a/theories/iron_logic/fcinv.v b/theories/iron_logic/fcinv.v
index b19a3d4..23b29a9 100644
--- a/theories/iron_logic/fcinv.v
+++ b/theories/iron_logic/fcinv.v
@@ -49,7 +49,7 @@ Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed.
 Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal).
 Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq).
 Arguments fcinv {_ _ _} _ _ _%I.
-Instance: Params (@fcinv) 5.
+Instance: Params (@fcinv) 5 := {}.
 
 Section fcinv.
 Context `{ironInvG Σ, invG Σ}.
diff --git a/theories/iron_logic/iron.v b/theories/iron_logic/iron.v
index fcb9174..e35b967 100644
--- a/theories/iron_logic/iron.v
+++ b/theories/iron_logic/iron.v
@@ -53,13 +53,13 @@ Class Uniform `{ironInvG Σ} (P : ironProp Σ) :=
   uniform π1 π2 : P (Some (π1 ⋅ π2)) ⊣⊢ P (Some π1) ∗ perm π2.
 Arguments Uniform {_ _} _%I.
 Hint Mode Uniform + + ! : typeclass_instances.
-Instance: Params (@Uniform) 2.
+Instance: Params (@Uniform) 2 := {}.
 
 Class ExistPerm `{ironInvG Σ} (P : ironProp Σ) :=
   exist_perm : P None ⊢ False.
 Arguments ExistPerm {_ _} _%I.
 Hint Mode ExistPerm + - ! : typeclass_instances.
-Instance: Params (@ExistPerm) 2.
+Instance: Params (@ExistPerm) 2 := {}.
 
 Definition iron_fupd_def `{ironInvG Σ, invG Σ} (E1 E2 : coPset)
     (P : ironProp Σ) : ironProp Σ := FracPred (λ π2, ∀ π1,
-- 
GitLab