Backport PR coq#15577: Pass more complete cstr in Rewrite.transitivit…

…y strategy

doc/changelog/04-tactics/15577-transitivity-opt-rew-rel.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  :tacn:`rewrite_strat` regression in 8.15.0 related to `Transitive` instances
+  (`#15577 <https://github.com/coq/coq/pull/15577>`_,
+  fixes `#15568 <https://github.com/coq/coq/issues/15568>`_,
+  by Gaëtan Gilbert).

plugins/ltac/rewrite.ml

@@ -1217,6 +1217,10 @@ let one_subterm = subterm false default_flags
 
 let transitivity state env unfresh cstr (res : rewrite_result_info) (next : 'a pure_strategy) :
     'a * rewrite_result =
+  let cstr = match cstr with
+    | _, Some _ -> cstr
+    | prop, None -> prop, get_opt_rew_rel res.rew_prf
+  in
   let state, nextres =
     next.strategy { state; env; unfresh; cstr;
                     term1 = res.rew_to;

test-suite/bugs/bug_15568.v

@@ -0,0 +1,18 @@
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.Classes.RelationClasses.
+
+Axiom mod_mod : forall a b : Z, Z.modulo (Z.modulo b a) a = Z.modulo b a.
+
+#[global] Hint Rewrite Z.add_0_r mod_mod : bu.
+
+Definition modEq (d:Z) := fun (a b :Z)=> Z.modulo a d = Z.modulo b d.
+
+#[global] Instance modEqR (d:Z): Reflexive  (modEq d). Admitted.
+#[global] Instance modEqT (d:Z): Transitive (modEq d). Admitted.
+
+Lemma foo d a e : (a mod d)%Z = e -> Z.modulo (Z.modulo a d + 0) d = e.
+Proof.
+  intro H.
+  rewrite_strat try (bottomup (hints bu)). (* Should not fail. *)
+  exact H.
+Qed.