diff --git a/opam.pins b/opam.pins
index 9db15430a363054e5037c0a9811c84766b3a8405..aa62552e97b44b8621effdf01c0d00c9949e4b90 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea64fd148b56e1c38c08c2954e76bfa2e75b4db9
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7b36d0e4c312b99b081f05b6575071b56bf12a55
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index a69d2e12221f3638875649ae77854d30105393a9..fd4c8c7b8dcee92f7c25a2fec285bb70b895320e 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
          | [ #(LitInt (0|1))] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto. Qed.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
 
   Global Instance bool_send : Send bool.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index e179a61b692bf8d0157933bba11154101b209260..d4d04fd1dc18d52686cadfac727c84619705d0c9 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
          | [ #(LitInt z)] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
+  Next Obligation. intros ? [|[[]|] []]; auto. Qed.
   Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
 
   Global Instance int_send : Send int.