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

bump Iris; fix build

parent e8a59e00
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 811a2081
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [ depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-06-14.8.bf9fd4f5") | (= "dev") } "coq-iris" { (= "branch.gen_proofmode.2018-06-15.3.d88d654b") | (= "dev") }
] ]
theories/adequacy.v
+ 1
− 1
View file @ 811a2081
...@@ -222,7 +222,7 @@ Proof. ...@@ -222,7 +222,7 @@ Proof.
iCombine "A" "B" as "AB". iCombine "A" "B" as "AB".
rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM. rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM.
match goal with match goal with
| |- coq_tactics.envs_entails _ (big_opM _ ?f ?g) => | |- environments.envs_entails _ (big_opM _ ?f ?g) =>
iApply (big_sepM_impl _ f with "[$AB]") iApply (big_sepM_impl _ f with "[$AB]")
end. end.
iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0. iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0.
......
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