Making a bit clearer that CoqIDE modifier menu is for global modifier change.

Indeed, one can change each item locally, but the preference menu is
only for changing the modifiers of a whole menu at once.

0 files changed, 0 insertions, 0 deletions