Commit e5c2be44 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 03c3a419
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-05-03.0.3b93f77c") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-23.3.7ae0b644") | (= "dev") }
]
......@@ -106,8 +106,7 @@ Section properties.
rewrite -own_op -auth_frag_op op_singleton pair_op agree_idemp. done.
- iIntros "[[Hl1 Ho1] [Hl2 Ho2]]".
iCombine "Hl1 Hl2" as "Hl". iFrame.
iCombine "Ho1 Ho2" as "Ho".
rewrite op_singleton pair_op agree_idemp. done.
iCombine "Ho1 Ho2" as "$".
Qed.
Global Instance mapsto_as_fractional l q x v :
AsFractional (mapsto l x q v) (λ q, mapsto l x q v)%I q.
......
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