Improving checks about the list separator in tactic notations.

In Tactic Notation and TACTIC EXTEND, when an argument not ending with
"_list_sep" was given with a separator, the separator was silently
ignored.

Now:
- we take it into account if it is a list (i.e. ending with "_list"), as if
  "_list_sep" was given, since after all, the "_sep" is useless in the name.
- we fail if there is a separator but it is not a "_list" or "_list_sep".

0 files changed, 0 insertions, 0 deletions