diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f8ba7a8e14a83e96634ace6e4e8b9a1e191c571f..f30a4c0a75c4b9d7c77ffc72557cb51995c36557 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -389,7 +389,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
 Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
 
 (* FromOp *)
-Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a â‹… b) a b.
+Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a â‹… b) a b | 100.
 Proof. by rewrite /FromOp. Qed.
 
 (* TODO: Worst case there could be a lot of backtracking on these instances,