Did the options include "don't change it" and did that perform worse than any given new name?
You really should take a look at their evaluation. It's quite comprehensive: https://coq.discourse.group/t/coq-community-survey-2022-resu...
From the post it seems that anglophones were significantly (as in statistically) more likely to change the name for exactly the reason one can imagine