diff --git a/opam b/opam index 295486ef449ea6726c6bb62e06d1c042735bbb51..3c841a39c251524bae86195bbcfc64d534cef55c 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 6a4ff897277b1e337694caec8e02d8bc246c1900..32dc76509fa7ecda24206a708d5af6a9ecd4f204 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 092f262e683cd35f4e4fb0bfbab30267217decf4..5cff46f7a3e1d75ca36d2e32f364fa17c5bfead8 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 b19a3d48a5ce80f7769374f63c9f9cb3c381363d..23b29a93cb4aa394f6e6d2e22b703b493e71770e 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 fcb9174c8c2c7e907b9e84d5c6bda21be02dd72b..e35b967cc6b21757b801f0374cf708f87332a33b 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,