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

1 files changed, 4 insertions, 2 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ca3c77aad..9809d4d09 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -89,10 +89,12 @@ type tomatch_type =
 (* spiwack: The first argument of [Pushed] is [true] for initial
    Pushed and [false] otherwise. Used to decide whether the term being
    matched on must be aliased in the variable case (only initial
-   Pushed need to be aliased). *)
+   Pushed need to be aliased). The first argument of [Alias] is [true]
+   if the alias was introduced by an initial pushed and [false]
+   otherwise.*)
 type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
-  | Alias of (Name.t * constr * (constr * types))
+  | Alias of (bool * (Name.t * constr * (constr * types)))
   | NonDepAlias
   | Abstract of int * rel_declaration