diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 546c65c07dfdeb9f0bdebeb6b77241ca938b5f3a..b8b184c06eb92f6d04ee306319829a985d28c910 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -909,12 +909,12 @@ Proof.
   intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
-Global Instance add_modal_except_0 P Q : AddModal (â—‡ P) P (â—‡ Q).
+Global Instance add_modal_except_0 P Q : AddModal (â—‡ P) P (â—‡ Q) | 1.
 Proof.
   intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
   by rewrite -except_0_sep wand_elim_r except_0_idemp.
 Qed.
-Global Instance add_modal_except_0_later P Q : AddModal (â—‡ P) P (â–· Q).
+Global Instance add_modal_except_0_later P Q : AddModal (â—‡ P) P (â–· Q) | 1.
 Proof.
   intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
   by rewrite -except_0_sep wand_elim_r except_0_later.