The highlighted search terms in the online refman are annoying

[ana-borges]

Description of the problem

The highlighted text can be very annoying, for example: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html?highlight=notation#coq:cmd.Notation

Note that the URL itself mentions the highlighting, and manually editing the URL gets rid of it. I wish there was a better way though.

We identified two possible avenues towards getting rid of it in this zulip discussion:

1. Include a button to hide the highlighting, like this. Sphinx has this feature, but not Read the Docs, and it seems it will continue not having it:
   A button for removing highlight content from the page readthedocs/sphinx_rtd_theme#816
   See also Proof of Concept: Hide search matches readthedocs/sphinx_rtd_theme#876
   This hypothetical button could perhaps be implemented on Coq's side.

2. Deploy the refman with Sphinx >= 4.5.0 in order to take advantage of Implement new search shortcuts. sphinx-doc/sphinx#9337. Note that 4.5.0 is the dev version at the time of writing.

cc. @cpitclaudel

[ana-borges]

Sphinx 4.5 is now more than a year old, so I think it's reasonable to go with that option.