Prevent spurious warnings about Arguments.

The Arguments command tends to emit the following warning even when
properly used:

  This command is just asserting the number and names of arguments of cons.
  If this is what you want add ': assert' to silence the warning. If you
  want to clear implicit arguments add ': clear implicits'. If you want to
  clear notation scopes add ': clear scopes'

In fact, even ': assert' does not silence it, contrarily to what the message
suggests.

0 files changed, 0 insertions, 0 deletions