Search Blacklist lemmas generated from Add Field

[Villetaneuse]

Description of the problem

I have noticed, while working with Reals that my Search queries are polluted by lemmas which (i think) were generated from an Add Field command.
These huge lemmas are

• RField_field_lemma[1-4]
• RField_ring_lemma[1-2]
• RField_lemma5 (sic)

I don't think they can be of any use to a human (they are completely unreadable), so I think it would be better if they were blacklisted from Search results.

Here is what appears at the end of a Search Rplus inside RIneq. command output:
Rfield_Search.txt

Coq Version

This is observed in upstream at this time (8.18+alpha) as well as in 8.16.

[SkySkimmer]

See also coq/coq#16327 which indicates maybe we could inline the lemmas where they're used instead of declaring them as constants (I didn't keep going because I didn't want to deal with the compat impact)

[SkySkimmer]

Why was this transferred? I thought the idea was to have Add Ring automatically add its lemmas to the blacklist