diff --git a/algebra/upred.v b/algebra/upred.v
index 465cfb505535f854cfe88478e4b66f1e1d6857b3..8080cab98d94a00578fec2c685023bc63f1da790 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -982,5 +982,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve always_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl : I.
+Hint Immediate iff_refl eq_refl : I.
 End uPred.