tactics.v: Fix parsing precedence for `select` tactic

I don't think a changelog entry here is needed since this tactic was added just a week ago.

added 1 commit

• 6eb05dfc - tactics.v: Fix parsing precedence for `select` tactic

Compare with previous version

unmarked as a Work In Progress

changed title from WIP: Fix parsing precedence in tactics.v to {+tactics.v: Fix parsing precedence for select tactic+}

changed the description

Ready @robbertkrebbers.

mentioned in commit 49b8abe5

merged

Thanks!