From 9c9d14b051e7ad45011057abff577aebdd79fe49 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 23 Jun 2018 18:36:58 +0200
Subject: [PATCH] decrease priority for rtc_reflexive instance

---
 theories/relations.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/relations.v b/theories/relations.v
index fa27e104..7b4370e1 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.
-- 
GitLab