Arguments needs a "simpl always" modifier

[JasonGross]

Description of the problem

Often / functions as simpl always but in fact it only behaves as such when not combined with !, see #4555 and #13800. Since the documentation of / indicates that it restricts reduction rather than allowing it, Arguments should gain an extra simpl always modifier which forces unfolding of the relevant constant except when forbidden by other modifiers (simpl nomatch, /, or !).

Coq Version

8.12

[Alizter]

So simpl always will become an alias for / right after the identifier, and is incompatible with !, simpl nomatch, simpl never and /?