decrease priority for rtc_reflexive instance

We give this instance a lower-than-usual priority because when it is applied to Reflexive ?, it leads to a new evar being created for R. Unfortunately, we cannot set Hint Mode for Reflexive in a way that just rules out Reflexive ? [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.

Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the IntoVal change as there may be other places where rtc_reflexive inadvertently gets chosen.

[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213

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.