Commit d4c7170c authored by Ralf Jung's avatar Ralf Jung

bump iris; small rename fix needed

parent 9c9943a2
Pipeline #9310 passed with stage
in 6 minutes and 29 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-04-27.2.1ab890fc") | (= "dev") }
"coq-iris" { (= "dev.2018-05-17.0.463474fb") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -43,7 +43,7 @@ Section ccounter.
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
is_ccounter γ₁ γ₂ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ₁ γ₂ q1 n1 is_ccounter γ₁ γ₂ q2 n2.
Proof.
apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
- iIntros "[? #?]".
iFrame "#"; iFrame.
- iIntros "[[? #?] [? _]]".
......@@ -128,4 +128,4 @@ Section ccounter.
simplify_eq. iApply "HΦ".
iFrame; iFrame "#".
Qed.
End ccounter.
\ No newline at end of file
End ccounter.
......@@ -593,7 +593,7 @@ Section ccounter.
Lemma is_ccounter_op γ q1 q2 (n1 n2 : nat) :
is_ccounter γ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ q1 n1 is_ccounter γ q2 n2.
Proof.
apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
- iIntros "[? #?]".
iFrame "#"; iFrame.
- iIntros "[[? #?] [? _]]".
......@@ -655,4 +655,4 @@ Section ccounter.
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
Qed.
End ccounter.
\ No newline at end of file
End ccounter.
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