diff --git a/theories/channel/multi_proofmode.v b/theories/channel/multi_proofmode.v
index 937f4b82849d649f8584899028781d0e9e3c2c51..a86ad89e209b7f9ee45f8805f1b38a8a1bd2df7b 100644
--- a/theories/channel/multi_proofmode.v
+++ b/theories/channel/multi_proofmode.v
@@ -194,14 +194,13 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
       |fail 1 "wp_recv: cannot find 'recv' in" e];
-    [try done|
-      solve_pointsto ()
+    [|solve_pointsto ()
        |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
     |tc_solve || fail 1 "wp_recv: cannot convert to telescope"
     |tc_solve
     |pm_reduce; simpl; tac_intros;
      tac Hnew;
-     wp_finish]
+     wp_finish];[try done|]
   | _ => fail "wp_recv: not a 'wp'"
   end.
 
@@ -311,7 +310,7 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
          |fail 1 "wp_send: cannot find 'send' in" e];
-       [try done|solve_pointsto ()
+       [|solve_pointsto ()
        |tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
        |tc_solve || fail 1 "wp_send: cannot convert to telescope"
        |pm_reduce; simpl; tac_exist;
@@ -323,7 +322,7 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
         | _ => notypeclasses refine (conj (eq_refl _) (conj _ _));
                 [iFrame Hs_frame; solve_done d
                 |wp_finish]
-        end]
+        end]; [try done|..]
      | _ => fail "wp_send: not a 'wp'"
      end
   | _ => fail "wp_send: only a single goal spec pattern supported"
@@ -357,26 +356,28 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
   wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
                 eexists x6; eexists x7; eexists x8) with pat.
 
-(* Section channel. *)
-(*   Context `{!heapGS Σ, !chanG Σ}. *)
-(*   Implicit Types p : iProto Σ. *)
-(*   Implicit Types TT : tele. *)
+Section channel.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
 
-(*   (* Lemma recv_test c p : *) *)
-(*   (*   {{{ c ↣ (<(Recv,0) @(x:Z)> MSG #x ; p) }}} *) *)
-(*   (*     recv c #0 *) *)
-(*   (*   {{{ x, RET #x; c ↣ p }}}. *) *)
-(*   (* Proof. *) *)
-(*   (*   iIntros (Φ) "Hc HΦ". *) *)
-(*   (*   wp_recv (x) as "_". *) *)
-(*   (*   { done. } *) *)
-(*   (*   iApply "HΦ". *) *)
-
-(*   Lemma send_test c p : *)
-(*     {{{ c ↣ (<(Send,0) @(x:Z)> MSG #x ; p) }}} *)
-(*       send c #0 #42 *)
-(*     {{{ x, RET #x; c ↣ p }}}. *)
-(*   Proof. *)
-(*     iIntros (Φ) "Hc HΦ". *)
-(*     wp_send (42%Z) with "[]". *)
-    
+  (* TODO: Why do the tactics not strip laters? *)
+  Lemma recv_test c p :
+    {{{ c ↣ (<(Recv,0) @(x:Z)> MSG #x ; p) }}}
+      recv c #0
+    {{{ x, RET #x; c ↣ p }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    wp_recv (x) as "_".
+  Admitted.
+
+  Lemma send_test c p :
+    {{{ c ↣ (<(Send,0) @(x:Z)> MSG #x ; p) }}}
+      send c #0 #42
+    {{{ x, RET #x; c ↣ p }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    wp_send (42%Z) with "[//]".
+  Admitted.
+
+End channel.
diff --git a/theories/channel/multi_proto_consistency_examples.v b/theories/channel/multi_proto_consistency_examples.v
index 0c3b22a81fe956ce9122a26a50eab06ea2167f9d..bdbb9ae3ad655a107747efb78ba5641c38d5d9ae 100644
--- a/theories/channel/multi_proto_consistency_examples.v
+++ b/theories/channel/multi_proto_consistency_examples.v
@@ -325,17 +325,16 @@ Section channel.
     iIntros (c2) "[Hc2 Hcs]".
     wp_smart_apply (wp_fork with "[Hc1]").
     { iIntros "!>".
-      (* TODO: Fix unification *)
-      wp_recv (x) as "_"; [done|].
-      wp_send with "[//]"; [done|].
+      wp_recv (x) as "_".
+      wp_send with "[//]".
       done. }
     wp_smart_apply (wp_fork with "[Hc2]").
     { iIntros "!>".
-      wp_recv (x) as "_"; [done|].
-      wp_send with "[//]"; [done|].
+      wp_recv (x) as "_".
+      wp_send with "[//]".
       done. }
-    wp_send with "[//]"; [done|].
-    wp_recv as "_"; [done|].
+    wp_send with "[//]".
+    wp_recv as "_".
     by iApply "HΦ".
   Qed.
 
@@ -347,10 +346,10 @@ Section example4.
   Definition iProto_example4 : gmap nat (iProto Σ) :=
     <[0 := (<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
             <(Recv, 2)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto]>
-      (<[1 := (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
-               <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; END)%proto]>
-         (<[2 := (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
-                  <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; END)%proto]>
+   (<[1 := (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+            <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; END)%proto]>
+   (<[2 := (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+            <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; END)%proto]>
             ∅)).
 
   Lemma iProto_example4_consistent :
@@ -575,19 +574,12 @@ Section proof.
     iIntros (c2) "[Hc2 Hcs]".
     wp_smart_apply (wp_fork with "[Hc1]").
     { iIntros "!>".
-      wp_recv (l x) as "Hl"; [done|].
-      wp_load. wp_store.
-      wp_send with "[$Hl]"; [done|].
-      done. }
+      wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[$Hl]". }
     wp_smart_apply (wp_fork with "[Hc2]").
     { iIntros "!>".
-      wp_recv (l x) as "Hl"; [done|].
-      wp_load. wp_store.
-      wp_send with "[$Hl]"; [done|].
-      done. }
-    wp_alloc l as "Hl".
-    wp_send with "[$Hl]"; [done|].
-    wp_recv as "Hl"; [done|]. wp_load. by iApply "HΦ".
+      wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[$Hl]". }
+    wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
+    by iApply "HΦ".
   Qed.
 
 End proof.