names carry the relevance

[gares]

After today's call I realized that the Rocq's Context.binder_annot are converted into Elpi's name dropping relevance, and the other way back setting it to Relevant. This PR keeps the relevance if given, or uses a relevance/quality variable if not.

TODO:

• propagate the change to all files
• test what happens now if the user calls the kernel without typing

CC @mattam82 @CohenCyril @tabareau

[JasonGross]

I got Claude to update the rest of the files at https://github.com/JasonGross/coq-elpi/tree/v3.3.1%2Bqvar (188450b). The only possibly-questionable thing I noticed was that it changed string->name from Easy to Full. (Note that coq.name-suffix has not been updated, I thiink.)

I am also running into some performance issues recompiling rocq-mathcomp-field (in fieldext.v), though I'm not sure if they are a result of this change or some other patch