Ensuring the right parsing of glob arguments, used by refine
and instantiate. Each of these tactics uses it at a different
parsing level, thus actually triggering a parsing error after
merging them. This fix implies some code duplication, which is
a pity. The separation between genargs and parsing entries should
be made one day.