Commit d768c93d authored by Ralf Jung's avatar Ralf Jung

update dependencies, fix TCs unfolding more than before

parent 2aa0b58c
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
"coq-iris" { (= "dev.2020-03-12.1.9f19f1ab") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -37,6 +37,7 @@ Section cnt_model.
Context `{!cntG Σ}.
Definition makeElem (q : Qp) (m : Z) : cntCmra := (q, to_agree m).
Typeclasses Opaque makeElem.
Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
(at level 20, q at level 50, format "γ ⤇[ q ] m") : bi_scope.
......@@ -59,7 +60,7 @@ Section cnt_model.
Global Instance makeElem_Exclusive m: Exclusive (makeElem 1 m).
Proof.
intros [y ?] [H _]. apply (exclusive_l _ _ H).
rewrite /makeElem. intros [y ?] [H _]. apply (exclusive_l _ _ H).
Qed.
Lemma makeElem_op p q n:
......
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