Commit 193d6230 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 6bbdfeb5
Pipeline #47443 passed with stage
in 18 minutes and 50 seconds
......@@ -9,8 +9,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/gpfsl.git"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
"coq-iris" { (= "dev.2021-05-21.0.e1eaa456") | (= "dev") }
"coq-orc11" { (= "dev.2021-05-20.0.94228b6e") | (= "dev") }
"coq-iris" { (= "dev.2021-05-26.5.13d5ab4f") | (= "dev") }
"coq-orc11" { (= "dev.2021-05-27.0.81b25747") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -545,28 +545,28 @@ Proof. by rewrite /FromForall -view_join_forall => <-. Qed.
IntoLaterN false n P Q IntoLaterN false n ({V} P) ({V} Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN => ->. by rewrite view_join_laterN. Qed.
#[global] Instance from_modal_id_view_join `(sel : A) P Q V :
FromModal modality_id sel P Q
FromModal modality_id sel ({V} P) ({V} Q) | 100.
Proof. by rewrite /FromModal /= =><-. Qed.
#[global] Instance from_modal_affinely_view_join `(sel : A) P Q V :
FromModal modality_affinely sel P Q
FromModal modality_affinely sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_join_affinely. Qed.
#[global] Instance from_modal_persistently_view_join `(sel : A) P Q V :
FromModal modality_persistently sel P Q
FromModal modality_persistently sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_join_persistently. Qed.
#[global] Instance from_modal_intuitionistically_view_join `(sel : A) P Q V :
FromModal modality_intuitionistically sel P Q
FromModal modality_intuitionistically sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_join_intuitionistically. Qed.
#[global] Instance from_modal_later_view_join `(sel : A) n P Q V :
FromModal (modality_laterN n) sel P Q
FromModal (modality_laterN n) sel ({V} P) ({V} Q).
Proof. rewrite /FromModal /= =><-. by rewrite view_join_laterN. Qed.
#[global] Instance from_modal_id_view_join φ `(sel : A) P Q V :
FromModal φ modality_id sel P Q
FromModal φ modality_id sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. rewrite -HPQ //. Qed.
#[global] Instance from_modal_affinely_view_join φ `(sel : A) P Q V :
FromModal φ modality_affinely sel P Q
FromModal φ modality_affinely sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_join_affinely. Qed.
#[global] Instance from_modal_persistently_view_join φ `(sel : A) P Q V :
FromModal φ modality_persistently sel P Q
FromModal φ modality_persistently sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_join_persistently. Qed.
#[global] Instance from_modal_intuitionistically_view_join φ `(sel : A) P Q V :
FromModal φ modality_intuitionistically sel P Q
FromModal φ modality_intuitionistically sel ({V} P) ({V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_join_intuitionistically. Qed.
#[global] Instance from_modal_later_view_join φ `(sel : A) n P Q V :
FromModal φ (modality_laterN n) sel P Q
FromModal φ (modality_laterN n) sel ({V} P) ({V} Q).
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_join_laterN. Qed.
#[global] Instance elim_modal_view_join_bupd_goal p p' φ P P' Q Q' V :
ElimModal φ p p' P P' (|==> {V} Q)%I (|==> {V} Q')%I
......@@ -672,28 +672,28 @@ Proof. by rewrite /FromForall -view_at_forall => <-. Qed.
IntoLaterN false n P Q IntoLaterN false n (@{V} P) (@{V} Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN => ->. by rewrite view_at_laterN. Qed.
#[global] Instance from_modal_id_view_at `(sel : A) P Q V :
FromModal modality_id sel P Q
FromModal modality_id sel (@{V} P) (@{V} Q) | 100.
Proof. by rewrite /FromModal /= =><-. Qed.
#[global] Instance from_modal_affinely_view_at `(sel : A) P Q V :
FromModal modality_affinely sel P Q
FromModal modality_affinely sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_at_affinely. Qed.
#[global] Instance from_modal_persistently_view_at `(sel : A) P Q V :
FromModal modality_persistently sel P Q
FromModal modality_persistently sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_at_persistently. Qed.
#[global] Instance from_modal_intuitionistically_view_at `(sel : A) P Q V :
FromModal modality_intuitionistically sel P Q
FromModal modality_intuitionistically sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =><-. by rewrite view_at_intuitionistically. Qed.
#[global] Instance from_modal_later_view_at `(sel : A) n P Q V :
FromModal (modality_laterN n) sel P Q
FromModal (modality_laterN n) sel (@{V} P) (@{V} Q).
Proof. rewrite /FromModal /= =><-. by rewrite view_at_laterN. Qed.
#[global] Instance from_modal_id_view_at φ `(sel : A) P Q V :
FromModal φ modality_id sel P Q
FromModal φ modality_id sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. rewrite -HPQ //. Qed.
#[global] Instance from_modal_affinely_view_at φ `(sel : A) P Q V :
FromModal φ modality_affinely sel P Q
FromModal φ modality_affinely sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_at_affinely. Qed.
#[global] Instance from_modal_persistently_view_at φ `(sel : A) P Q V :
FromModal φ modality_persistently sel P Q
FromModal φ modality_persistently sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_at_persistently. Qed.
#[global] Instance from_modal_intuitionistically_view_at φ `(sel : A) P Q V :
FromModal φ modality_intuitionistically sel P Q
FromModal φ modality_intuitionistically sel (@{V} P) (@{V} Q) | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_at_intuitionistically. Qed.
#[global] Instance from_modal_later_view_at φ `(sel : A) n P Q V :
FromModal φ (modality_laterN n) sel P Q
FromModal φ (modality_laterN n) sel (@{V} P) (@{V} Q).
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // view_at_laterN. Qed.
#[global] Instance elim_modal_view_at_bupd_goal p p' φ P P' Q Q' V :
ElimModal φ p p' P P' (|==> @{V} Q)%I (|==> @{V} Q')%I
......
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