Fixing factorization of recursive notations in the case of an atomic separator.

This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.

To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.

0 files changed, 0 insertions, 0 deletions