I am confused about what are arguments in Coq. I have read the documentation, but I have not found a formal definition of arguments thus having some confusion.
The documentation defines the syntax intros ident+, therefore according to the definition, the argument for intros n m can only be n m. A Single n is not the argument of intros n m.
Is there anything wrong with my understanding?