bump Iris for wp_finish changes

coq-iris-tutorial-popl18.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git"
 synopsis: "The Iris tutorial at POPL 2018"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2020-11-11.2.dc3b7961") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

exercises/ex_01_swap.v

@@ -71,7 +71,7 @@ Lemma swap_spec_2 x y v1 v2 :
 Proof.
   iIntros (Φ) "[??] Post".
   wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
-  iApply "Post". iFrame.
+  iApply "Post". iFrame. done.
 Qed.
 
 (* We can further automate the lemma by defining a simple Ltac tactic for
@@ -89,7 +89,7 @@ Lemma swap_spec_2_more_automation x y v1 v2 :
   {{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
 Proof.
   iIntros (Φ) "[??] Post". wp_exec.
-  iApply "Post". iFrame.
+  iApply "Post". iFrame. done.
 Qed.
 
 Lemma rotate_r_spec x y z v1 v2 v3 :

solutions/ex_01_swap.v

@@ -71,7 +71,7 @@ Lemma swap_spec_2 x y v1 v2 :
 Proof.
   iIntros (Φ) "[??] Post".
   wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
-  iApply "Post". iFrame.
+  iApply "Post". iFrame. done.
 Qed.
 
 (* We can further automate the lemma by defining a simple Ltac tactic for
@@ -89,7 +89,7 @@ Lemma swap_spec_2_more_automation x y v1 v2 :
   {{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
 Proof.
   iIntros (Φ) "[??] Post". wp_exec.
-  iApply "Post". iFrame.
+  iApply "Post". iFrame. done.
 Qed.
 
 Lemma rotate_r_spec x y z v1 v2 v3 :