diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index f850513206d69ddfe017c721b59feefd14828bd8..f9540df97c0901a6544b2d152dfd1fd18ab41e17 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -175,6 +175,9 @@ Section proofmode_classes.
   Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
   Proof. rewrite /IntoModal. apply fupd_intro. Qed.
 
+  (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
+     it is not taken when the first parameter is not specified (in
+     spec. patterns). *)
   Global Instance elim_modal_bupd_fupd E1 E2 P Q :
     ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
   Proof.