Bump Iris.

coq-iris-examples.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-02-12.0.ae905a7d") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
   "coq-autosubst" { = "dev" }
   "coq-iris-string-ident"
 ]

theories/lecture_notes/ccounter.v

@@ -44,7 +44,7 @@ Section ccounter.
   Lemma is_ccounter_op γ₁ γ₂ ℓ q1 q2 (n1 n2 : nat) :
     is_ccounter γ₁ γ₂ ℓ (q1 + q2) (n1 + n2) ⊣⊢ is_ccounter γ₁ γ₂ ℓ q1 n1 ∗ is_ccounter γ₁ γ₂ ℓ q2 n2.
   Proof.
-    apply bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
+    apply bi.equiv_entails; split; rewrite /is_ccounter frac_auth_frag_op own_op.
     - iIntros "[? #?]".
       iFrame "#"; iFrame.
     - iIntros "[[? #?] [? _]]".

theories/lecture_notes/coq_intro_example_2.v

@@ -597,7 +597,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 bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
+    apply bi.equiv_entails; split; rewrite /is_ccounter frac_auth_frag_op own_op.
     - iIntros "[? #?]".
       iFrame "#"; iFrame.
     - iIntros "[[? #?] [? _]]".