Commit f7c8b3a3 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris, make compatible with Coq master.

parent 4069fe36
Pipeline #14373 passed with stage
in 5 minutes and 48 seconds
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") } "coq-iris" { (= "dev.2019-02-01.0.de7eab03") | (= "dev") }
] ]
...@@ -35,8 +35,8 @@ Definition vfrac_auth_frag {A : cmraT} (q : Qp) (x : A) : vfrac_authR A := ...@@ -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. Typeclasses Opaque vfrac_auth_auth vfrac_auth_frag.
Instance: Params (@vfrac_auth_auth) 2. Instance: Params (@vfrac_auth_auth) 2 := {}.
Instance: Params (@vfrac_auth_frag) 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_auth q a) (at level 10, format "●?{ q } a").
Notation "◯?{ q } a" := (vfrac_auth_frag q a) (at level 10, format "◯?{ q } a"). Notation "◯?{ q } a" := (vfrac_auth_frag q a) (at level 10, format "◯?{ q } a").
......
...@@ -269,7 +269,7 @@ Class FObjective {PROP : bi} (P : fracPred PROP) := ...@@ -269,7 +269,7 @@ Class FObjective {PROP : bi} (P : fracPred PROP) :=
Arguments FObjective {_} _%I. Arguments FObjective {_} _%I.
Arguments fobjective_at {_} _%I {_}. Arguments fobjective_at {_} _%I {_}.
Hint Mode FObjective + ! : typeclass_instances. Hint Mode FObjective + ! : typeclass_instances.
Instance: Params (@FObjective) 1. Instance: Params (@FObjective) 1 := {}.
(** Primitive facts that cannot be deduced from the BI structure. *) (** Primitive facts that cannot be deduced from the BI structure. *)
Section bi_facts. Section bi_facts.
......
...@@ -49,7 +49,7 @@ Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed. ...@@ -49,7 +49,7 @@ Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed.
Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal). Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal).
Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq). Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq).
Arguments fcinv {_ _ _} _ _ _%I. Arguments fcinv {_ _ _} _ _ _%I.
Instance: Params (@fcinv) 5. Instance: Params (@fcinv) 5 := {}.
Section fcinv. Section fcinv.
Context `{ironInvG Σ, invG Σ}. Context `{ironInvG Σ, invG Σ}.
......
...@@ -53,13 +53,13 @@ Class Uniform `{ironInvG Σ} (P : ironProp Σ) := ...@@ -53,13 +53,13 @@ Class Uniform `{ironInvG Σ} (P : ironProp Σ) :=
uniform π1 π2 : P (Some (π1 π2)) P (Some π1) perm π2. uniform π1 π2 : P (Some (π1 π2)) P (Some π1) perm π2.
Arguments Uniform {_ _} _%I. Arguments Uniform {_ _} _%I.
Hint Mode Uniform + + ! : typeclass_instances. Hint Mode Uniform + + ! : typeclass_instances.
Instance: Params (@Uniform) 2. Instance: Params (@Uniform) 2 := {}.
Class ExistPerm `{ironInvG Σ} (P : ironProp Σ) := Class ExistPerm `{ironInvG Σ} (P : ironProp Σ) :=
exist_perm : P None False. exist_perm : P None False.
Arguments ExistPerm {_ _} _%I. Arguments ExistPerm {_ _} _%I.
Hint Mode ExistPerm + - ! : typeclass_instances. Hint Mode ExistPerm + - ! : typeclass_instances.
Instance: Params (@ExistPerm) 2. Instance: Params (@ExistPerm) 2 := {}.
Definition iron_fupd_def `{ironInvG Σ, invG Σ} (E1 E2 : coPset) Definition iron_fupd_def `{ironInvG Σ, invG Σ} (E1 E2 : coPset)
(P : ironProp Σ) : ironProp Σ := FracPred (λ π2, π1, (P : ironProp Σ) : ironProp Σ := FracPred (λ π2, π1,
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment