Commit 0a74ae14 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (ident_name changes).

parent 0c069e7d
Pipeline #31933 passed with stage
in 19 minutes and 12 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2020-06-18.3.5f98a0bf") | (= "dev") }
"coq-iris" { (= "dev.2020-07-21.2.e989ad6b") | (= "dev") }
]
......@@ -1233,12 +1233,16 @@ Section proto.
(** The instances below make it possible to use the tactics [iIntros],
[iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *)
Global Instance iProto_le_from_forall_l {A} a (m1 : A iMsg Σ V) m2 :
FromForall ((<? x> m1 x) (<a> m2)) (λ x, (<?> m1 x) (<a> m2))%I | 10.
Proof. apply iProto_le_exist_elim_l. Qed.
Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A iMsg Σ V) :
FromForall ((<a> m1) (<! x> m2 x)) (λ x, (<a> m1) (<!> m2 x))%I | 11.
Proof. apply iProto_le_exist_elim_r. Qed.
Global Instance iProto_le_from_forall_l {A} a (m1 : A iMsg Σ V) m2 name :
AsIdentName m1 name
FromForall (iProto_message Recv (iMsg_exist m1) (<a> m2))
(λ x, (<?> m1 x) (<a> m2))%I name | 10.
Proof. intros _. apply iProto_le_exist_elim_l. Qed.
Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A iMsg Σ V) name :
AsIdentName m2 name
FromForall ((<a> m1) iProto_message Send (iMsg_exist m2))
(λ x, (<a> m1) (<!> m2 x))%I name | 11.
Proof. intros _. apply iProto_le_exist_elim_r. Qed.
Global Instance iProto_le_from_wand_l a m v P p :
TCIf (TCEq P True%I) False TCTrue
......
......@@ -497,12 +497,14 @@ Section subtyping_rules.
[iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
These instances have higher precedence than the ones in [proto.v] to avoid
needless unfolding of the subtyping relation. *)
Global Instance lty_le_from_forall_l k (M : lty Σ k lmsg Σ) (S : lsty Σ) :
FromForall ((<?? X> M X) <: S) (λ X, (<??> M X) <: S)%I | 0.
Proof. apply lty_le_exist_elim_l. Qed.
Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k lmsg Σ) :
FromForall (S <: (<!! X> M X)) (λ X, S <: (<!!> M X))%I | 1.
Proof. apply lty_le_exist_elim_r. Qed.
Global Instance lty_le_from_forall_l k (M : lty Σ k lmsg Σ) (S : lsty Σ) name :
AsIdentName M name
FromForall (lty_message Recv (lty_msg_exist M) <: S) (λ X, (<??> M X) <: S)%I name | 0.
Proof. intros _. apply lty_le_exist_elim_l. Qed.
Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k lmsg Σ) name :
AsIdentName M name
FromForall (S <: lty_message Send (lty_msg_exist M)) (λ X, S <: (<!!> M X))%I name | 1.
Proof. intros _. apply lty_le_exist_elim_r. Qed.
Global Instance lty_le_from_exist_l k (M : lty Σ k lmsg Σ) S :
FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
......
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