Fix compilation of pattern matching wrt variables: alias.

Aliases (as clause) are a bit tricky.

In Goal True,

refine match 0 with
| S n as p => _
| _ => I
end

Must produce the goal

n:nat, p := S n : nat |- True

However, in the deep branches:

refine match 0 with
| S (S n as p) => _
| _ => I
end

The alias is used to give a name to the variable of the first S :

p:nat, n:nat |- True

Before this patch, the goal would be

p:nat, n:nat, p:=p : nat |- True

Alias was used both to name the variable of the first S and to alias it.