Skip to content
Snippets Groups Projects
Commit ebddbb7f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 360cb44f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ ebddbb7f
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 646bfc85e7ea6313e62feecf4ebcbcd76a186e71
theories/typing/function.v
+ 1
− 1
View file @ ebddbb7f
......@@ -274,7 +274,7 @@ Section typing.
{ iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
+ iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=. iSplitL.
iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
{ iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
+ iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment