diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 4b2a013f6fc5abb7c2842f6335699543fa2862c7..9c7e4e32f6c47bc1a2364a73ec849e49d1848514 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -127,7 +127,7 @@ Section dfrac.
     intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
     - apply (Qp_not_plus_ge 1 q).
-    - intros []%irreflexivity. apply _.
+    - intros []%(irreflexivity _).
     - move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
   Qed.