Skip to content

GitLab

E
examples
Commit bcfa9d23 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Bump Iris (sbi removal).

parent 2b52b152
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
opam
View file @ bcfa9d23
...@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git" ...@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris" synopsis: "A collection of case studies for Iris"
depends: [ depends: [
"coq-iris" { (= "dev.2020-05-18.2.fdda97e8") | (= "dev") } "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident" "coq-iris-string-ident"
] ]
......
theories/barrier/example_joining_existentials.v
View file @ bcfa9d23
...@@ -58,7 +58,7 @@ Proof. ...@@ -58,7 +58,7 @@ Proof.
iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']". iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
iAssert (▷ (x ≡ x'))%I as "Hxx". iAssert (▷ (x ≡ x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'". { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=. rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
rewrite -{2}[x]oFunctor_map_id -{2}[x']oFunctor_map_id. rewrite -{2}[x]oFunctor_map_id -{2}[x']oFunctor_map_id.
assert (HF : oFunctor_map F (cid, cid) ≡ oFunctor_map F (iProp_fold (Σ:=Σ) ◎ assert (HF : oFunctor_map F (cid, cid) ≡ oFunctor_map F (iProp_fold (Σ:=Σ) ◎
iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)). iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
......
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