The Standard Library should not be adding transitivity and symmetry hints to `core`

Description of the problem

https://github.com/coq/coq/blob/cb296e38848656025f68527e017e22d1e781f716/theories/Structures/Equalities.v#L57-L60

This means that any time I extend a module with this type via <+, core gets permanently polluted with this endlessly looping instances. For example:

Require Import Coq.Structures.Equalities.

Module Foo (E : EqualityTypeOrig).
  Module E' := E (* possibly to add extra things to E with <+ *).
End Foo.

Module Bar <: EqualityTypeOrig.
  Definition t := nat.
  Definition eq := @eq nat.
  Definition eq_refl := @eq_refl nat.
  Definition eq_sym := @eq_sym nat.
  Definition eq_trans := @eq_trans nat.
End Bar.

Module F := Foo Bar.
Print HintDb core.
(* For F.E'.eq ->   simple apply F.E'.eq_refl(level 0, pattern
                 F.E'.eq ?META535 ?META535, id 0)
                 simple apply F.E'.eq_sym ; trivial(level 1, pattern
                 F.E'.eq ?META530 ?META529, id 0)
                 simple eapply F.E'.eq_trans(level 3, pattern
                 F.E'.eq ?META536 ?META538, id 0)
*)

These should not be in core, and any code that relies on them being in core can be fixed in a backwards compatible way by locally adding the hints to core.

Coq Version

8.15

Start with theories/Structures/Equalities.v at lines 57-60 and reproduce the module-extension example from the issue. Inspect Print HintDb core before and after the reproduction; done means the transitivity and symmetry hints described in the report are no longer added to core while existing behavior remains accounted for.