3 ms·

Did the options include "don't change it" and did that perform worse than any given new name?

• vslira 2y ago
  It doesn’t seem so, but by a slight majority on overall respondents it seems like changing the name was favored. 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
• Cu3PO42 2y ago
  Whether the name should be changed was a separate question and there was a slight majority in favor of changing it. Among respondents who favored changing the name, there were options that were more liked than disliked, but not by the entire community. You really should take a look at their evaluation. It's quite comprehensive: https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001 https://coq.discourse.group/t/coq-community-survey-2022-resu...