More goal selection tacticals.

A goal selector is of the form:

  `g1~g2`

where `g1` is an inclusive goal set (defaults to the full set) and `g2`
is an exclusive goal set (defaults to the empty set - in that case, `~`
is optional).

A goal index `i` is selected by a goal selector `g1~g2` if it is in `g1`
and not in `g2`.

A goal set can be

  - a singleton goal index (`i`). If `i` is negative, it selects the
    `|i|`th, counting from the end;
  - a in inclusive range of goal index (`i1..i2`);
  - a union of two goal sets (`g1,g2`)

Goal selectors can be found in:

  - rewrite rules: `rewrite gs:rw`
        applies `rw` on goals selected by `gs`
  - in chaining: `t1; gs:t2`
        applies `t2` on goals selected by `gs`
  - in sub-chaining: `t; [gs1: t1 | ... | gsn:tn else td]`
        for each subgoal, applies the first `ti` (from left to right)
        whose goal selector `gsi` selects the subgoal index, or applies
        `td` if no goal selectors matched the subgoal index. The `else`
        branch is optional.

[close #17137]
Merge branch '1.0' of git://ci.easycrypt.info/easycrypt into 1.0