diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index cf118ab660de11b0d9ac2b96398f1ec6d505c019..34ee47b9143fab2fa0ffcae2d34c05f782c0d11b 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -22,7 +22,7 @@ Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
 Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.
 
 Global Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q :
   IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).