diff --git a/theories/relations.v b/theories/relations.v
index fa27e104c6c741ae2424f54505d0b1186d6b3d2d..7b4370e16a9f1ea75052d02e02c1e9b193846f06 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -65,7 +65,14 @@ Section rtc.
Hint Constructors rtc nsteps bsteps tc.
- Global Instance rtc_reflexive: Reflexive (rtc R).
+ (* We give this instance a lower-than-usual priority because [setoid_rewrite]
+ queries for [@Reflexive Prop ?r] in the hope of [iff_reflexive] getting
+ picked as the instance. [rtc_reflexive] overlaps with that, leading to
+ backtracking. We cannot set [Hint Mode] because that query must not fail,
+ but we can at least avoid picking [rtc_reflexive].
+
+ See Coq bug https://github.com/coq/coq/issues/7916. *)
+ Global Instance rtc_reflexive: Reflexive (rtc R) | 10.
Proof. exact (@rtc_refl A R). Qed.
Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z.
Proof. induction 1; eauto. Qed.