Remove uses of iStartProof, which is intended as being an internal tactic.

theories/typing/bool.v

@@ -13,7 +13,7 @@ Section bool.
          | [ #(LitInt (0|1))] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; iStartProof; auto. Qed.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
 
   Global Instance bool_send : Send bool.

theories/typing/int.v

@@ -12,7 +12,7 @@ Section int.
          | [ #(LitInt z)] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[]|] []]; iStartProof; auto. Qed.
+  Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
 
   Global Instance int_send : Send int.

theories/typing/type_context.v

@@ -56,8 +56,7 @@ Section type_context.
     destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
     destruct v0; try discriminate; [].
     destruct l; try discriminate; [].
-    intros [=<-]. iStartProof. wp_bind p1.
-    iApply (wp_wand with "[]").
+    intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
     { iApply IHp1. done. }
     iIntros (v) "%". subst v. wp_op. done.
   Qed.