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.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17022 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions