diff --git a/opam.pins b/opam.pins
index 9087d1ed13556140819293adf4d9c13459b4c69d..2c200453f67a9f2301754445d21ca0e7403bc5a6 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2774efcd9701526458946946ddfcd3d14616cfb7..9bcb847f67c12eb2bd80ccd2c3e3fff26c9ba45f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -376,7 +376,7 @@ End type_contractive.
 (* Tactic automation. *)
 Ltac f_type_equiv :=
   first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
-          match goal with | |- @dist_later ?A ?n ?x ?y =>
+          match goal with | |- @dist_later ?A _ ?n ?x ?y =>
                             destruct n as [|n]; [exact I|change (@dist A _ n x y)]
           end ].
 Ltac solve_type_proper :=