Skip to content
Snippets Groups Projects
Commit b91fe227 authored by Ralf Jung's avatar Ralf Jung
Browse files

update to latest Iris

parent 07f64306
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ b91fe227
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 039f9fd5f753337034dcbfbbdb311cebdfa93acf coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c798ff4f78cd663c2a710b0af4e7af063b35580a
theories/typing/lft_contexts.v
+ 1
− 1
View file @ b91fe227
...@@ -342,7 +342,7 @@ Section lft_contexts. ...@@ -342,7 +342,7 @@ Section lft_contexts.
iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done. iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done.
iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done. iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done.
destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q. destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q.
rewrite !fractional (fractional_half_equiv qE) /elctx_interp big_sepL_app. rewrite !fractional [elctx_interp E qE]fractional_half /elctx_interp big_sepL_app.
iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]". iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]".
iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame. iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame.
Qed. Qed.
......
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