Unset Asymmetric Patterns

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

17 files changed, 192 insertions, 202 deletions

diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
index c8f7726876..445ffac8cb 100644
--- a/test-suite/success/Case11.v
+++ b/test-suite/success/Case11.v
@@ -7,7 +7,7 @@ Variables (Alpha : Set) (Beta : Set).
 
 Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) :
   Alpha * Beta := match c with
-                  | existS a b => (a, b)
+                  | existS _ a b => (a, b)
                   end.
 
 End A.
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 729ab824f8..55e17facce 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -68,6 +68,6 @@ Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
 Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m)
   {struct l} : nat :=
   match l with
-  | nil''' => 0
-  | cons''' _ m l0 => S (length''' A a m l0)
+  | nil''' _ _ => 0
+  | @cons''' _ _ _ _ m l0 => S (length''' A a m l0)
   end.
diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v
index 77016bbfe6..ce9a0ecb4a 100644
--- a/test-suite/success/Case16.v
+++ b/test-suite/success/Case16.v
@@ -5,6 +5,6 @@
 Check
   (fun x : {b : bool | if b then True else False} =>
    match x return (let (b, _) := x in if b then True else False) with
-   | exist true y => y
-   | exist false z => z
+   | exist _ true y => y
+   | exist _ false z => z
    end).
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v
index 66af9e0d36..861d04668f 100644
--- a/test-suite/success/Case17.v
+++ b/test-suite/success/Case17.v
@@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A.
 
 Check
   (match rec l0 (HHH _) with
-   | inleft (existS (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) =>
+   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _) => inright _ (HHH _)
+   | inleft (existS _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
@@ -39,10 +39,10 @@ Check
             {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
             {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
    match rec l0 (HHH _) with
-   | inleft (existS (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) =>
+   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _) => inright _ (HHH _)
+   | inleft (existS _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v
index 6e4b20031b..f95598aadb 100644
--- a/test-suite/success/Case7.v
+++ b/test-suite/success/Case7.v
@@ -12,6 +12,6 @@ Parameter
 Type
   (fun (A : Set) (l : List A) =>
    match l return (Empty A l \/ ~ Empty A l) with
-   | Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A)
-   | Cons a y as b => or_intror (Empty A b) (inv_Empty A a y)
+   | Nil _ => or_introl (~ Empty A (Nil A)) (intro_Empty A)
+   | Cons _ a y as b => or_intror (Empty A b) (inv_Empty A a y)
    end).
diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v
index a8534a0b99..e34e5b9baa 100644
--- a/test-suite/success/Case9.v
+++ b/test-suite/success/Case9.v
@@ -36,10 +36,10 @@ Parameter
 Fixpoint eqlongdec (x y : List nat) {struct x} :
  eqlong x y \/ ~ eqlong x y :=
   match x, y return (eqlong x y \/ ~ eqlong x y) with
-  | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
-  | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
-  | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
-  | Cons a x as L1, Cons b y as L2 =>
+  | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
+  | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
+  | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x)
+  | Cons _ a x as L1, Cons _ b y as L2 =>
       match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
       | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
       | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
@@ -49,10 +49,10 @@ Fixpoint eqlongdec (x y : List nat) {struct x} :
 
 Type
   match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
-  | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
-  | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
-  | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
-  | Cons a x as L1, Cons b y as L2 =>
+  | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
+  | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
+  | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x)
+  | Cons _ a x as L1, Cons _ b y as L2 =>
       match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
       | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
       | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v
index 543ca0c924..cf102486a6 100644
--- a/test-suite/success/Cases-bug1834.v
+++ b/test-suite/success/Cases-bug1834.v
@@ -7,7 +7,7 @@ Definition T := sig P.
 Parameter Q : T -> Prop.
 Definition U := sig Q.
 Parameter a : U.
-Check (match a with exist (exist tt e2) e3 => e3=e3 end).
+Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end).
 
 (* There is still a form submitted by Pierre Corbineau (#1834) which fails *)
 
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index c9a3c08efe..257c55fd80 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -309,43 +309,43 @@ Type
 Type
   (fun l : List nat =>
    match l return (List nat) with
-   | Nil => Nil nat
-   | Cons a l => l
+   | Nil _ => Nil nat
+   | Cons _ a l => l
    end).
 
 Type (fun l : List nat => match l with
-                          | Nil => Nil nat
-                          | Cons a l => l
+                          | Nil _ => Nil nat
+                          | Cons _ a l => l
                           end).
 
 Type match Nil nat return nat with
-     | Nil => 0
-     | Cons a l => S a
+     | Nil _ => 0
+     | Cons _ a l => S a
      end.
 Type match Nil nat with
-     | Nil => 0
-     | Cons a l => S a
+     | Nil _ => 0
+     | Cons _ a l => S a
      end.
 
 Type match Nil nat return (List nat) with
-     | Cons a l => l
+     | Cons _ a l => l
      | x => x
      end.
 
 Type match Nil nat with
-     | Cons a l => l
+     | Cons _ a l => l
      | x => x
      end.
 
 Type
   match Nil nat return (List nat) with
-  | Nil => Nil nat
-  | Cons a l => l
+  | Nil _ => Nil nat
+  | Cons _ a l => l
   end.
 
 Type match Nil nat with
-     | Nil => Nil nat
-     | Cons a l => l
+     | Nil _ => Nil nat
+     | Cons _ a l => l
      end.
 
 
@@ -353,8 +353,8 @@ Type
   match 0 return nat with
   | O => 0
   | S x => match Nil nat return nat with
-           | Nil => x
-           | Cons a l => x + a
+           | Nil _ => x
+           | Cons _ a l => x + a
            end
   end.
 
@@ -362,8 +362,8 @@ Type
   match 0 with
   | O => 0
   | S x => match Nil nat with
-           | Nil => x
-           | Cons a l => x + a
+           | Nil _ => x
+           | Cons _ a l => x + a
            end
   end.
 
@@ -372,8 +372,8 @@ Type
    match y with
    | O => 0
    | S x => match Nil nat with
-            | Nil => x
-            | Cons a l => x + a
+            | Nil _ => x
+            | Cons _ a l => x + a
             end
    end).
 
@@ -381,8 +381,8 @@ Type
 Type
   match 0, Nil nat return nat with
   | O, x => 0
-  | S x, Nil => x
-  | S x, Cons a l => x + a
+  | S x, Nil _ => x
+  | S x, Cons _ a l => x + a
   end.
 
 
@@ -597,71 +597,60 @@ Type
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l return nat with
-   | Niln => 0
-   | Consn n a Niln => 0
-   | Consn n a (Consn m b l) => n + m
+   | Niln _ => 0
+   | Consn _ n a (Niln _) => 0
+   | Consn _ n a (Consn _ m b l) => n + m
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l with
-   | Niln => 0
-   | Consn n a Niln => 0
-   | Consn n a (Consn m b l) => n + m
+   | Niln _ => 0
+   | Consn _ n a (Niln _) => 0
+   | Consn _ n a (Consn _ m b l) => n + m
    end).
 
-(* This example was deactivated in Cristina's code
-
 Type
   (fun (A:Set) (n:nat) (l:Listn A n) =>
     match l return Listn A O with
-      | Niln  as b => b
-      | Consn  n a (Niln  as b) => (Niln A)
-      | Consn  n a (Consn m b l) => (Niln A)
+      | Niln _ as b => b
+      | Consn _  n a (Niln _ as b) => (Niln A)
+      | Consn _ n a (Consn _ m b l) => (Niln A)
     end).
-*)
-
-(* This one is (still) failing: too weak unification
 
+(*
 Type
   (fun (A:Set) (n:nat) (l:Listn A n) =>
     match l with
-      | Niln  as b => b
-      | Consn  n a (Niln  as b) => (Niln A)
-      | Consn  n a (Consn m b l) => (Niln A)
+      | Niln _ as b => b
+      | Consn _ n a (Niln _ as b) => (Niln A)
+      | Consn _ n a (Consn _ m b l) => (Niln A)
     end).
 *)
 
-(* This one is failing: alias L not chosen of the right type
-
 Type
   (fun (A:Set) (n:nat) (l:Listn A n) =>
     match l return Listn A (S 0) with
-      | Niln  as b => Consn A O O b
-      | Consn n a Niln as L => L
-      | Consn n a _ => Consn A O O (Niln A)
+      | Niln _ as b => Consn A O O b
+      | Consn _ n a (Niln _) as L => L
+      | Consn _ n a _ => Consn A O O (Niln A)
     end).
-*)
-
-(******** This example (still) failed
 
 Type
   (fun (A:Set) (n:nat) (l:Listn A n) =>
     match l return Listn A (S 0) with
-      | Niln  as b => Consn A O O b
-      | Consn n a Niln as L => L
-      | Consn n a _ => Consn A O O (Niln A)
+      | Niln _ as b => Consn A O O b
+      | Consn _ n a (Niln _) as L => L
+      | Consn _ n a _ => Consn A O O (Niln A)
     end).
 
-**********)
-
 (* To test treatment of as-patterns in depth *)
 Type
   (fun (A : Set) (l : List A) =>
    match l with
-   | Nil as b => Nil A
-   | Cons a Nil as L => L
-   | Cons a (Cons b m) as L => L
+   | Nil _ as b => Nil A
+   | Cons _ a (Nil _) as L => L
+   | Cons _ a (Cons _ b m) as L => L
    end).
 
 
@@ -704,40 +693,40 @@ Type
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l with
-   | Niln as b => l
+   | Niln _ as b => l
    | _ => l
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l return (Listn A n) with
-   | Niln => l
-   | Consn n a Niln => l
-   | Consn n a (Consn m b c) => l
+   | Niln _ => l
+   | Consn _ n a (Niln _) => l
+   | Consn _ n a (Consn _ m b c) => l
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l with
-   | Niln => l
-   | Consn n a Niln => l
-   | Consn n a (Consn m b c) => l
+   | Niln _ => l
+   | Consn _ n a (Niln _) => l
+   | Consn _ n a (Consn _ m b c) => l
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l return (Listn A n) with
-   | Niln as b => l
-   | Consn n a (Niln as b) => l
-   | Consn n a (Consn m b _) => l
+   | Niln _ as b => l
+   | Consn _ n a (Niln _ as b) => l
+   | Consn _ n a (Consn _ m b _) => l
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l with
-   | Niln as b => l
-   | Consn n a (Niln as b) => l
-   | Consn n a (Consn m b _) => l
+   | Niln _ as b => l
+   | Consn _ n a (Niln _ as b) => l
+   | Consn _ n a (Consn _ m b _) => l
    end).
 
 
@@ -770,40 +759,40 @@ Type match LeO 0 with
 Type
   (fun (n : nat) (l : Listn nat n) =>
    match l return nat with
-   | Niln => 0
-   | Consn n a l => 0
+   | Niln _ => 0
+   | Consn _ n a l => 0
    end).
 
 
 Type
   (fun (n : nat) (l : Listn nat n) =>
    match l with
-   | Niln => 0
-   | Consn n a l => 0
+   | Niln _ => 0
+   | Consn _ n a l => 0
    end).
 
 
 Type match Niln nat with
-     | Niln => 0
-     | Consn n a l => 0
+     | Niln _ => 0
+     | Consn _ n a l => 0
      end.
 
 Type match LE_n 0 return nat with
-     | LE_n => 0
-     | LE_S m h => 0
+     | LE_n _ => 0
+     | LE_S _ m h => 0
      end.
 
 
 Type match LE_n 0 with
-     | LE_n => 0
-     | LE_S m h => 0
+     | LE_n _ => 0
+     | LE_S _ m h => 0
      end.
 
 
 
 Type match LE_n 0 with
-     | LE_n => 0
-     | LE_S m h => 0
+     | LE_n _ => 0
+     | LE_S _ m h => 0
      end.
 
 
@@ -825,16 +814,17 @@ Type
 
 Type
   match Niln nat return nat with
-  | Niln => 0
-  | Consn n a Niln => n
-  | Consn n a (Consn m b l) => n + m
+  | Niln _ => 0
+  | Consn _ n a (Niln _
+) => n
+  | Consn _ n a (Consn _ m b l) => n + m
   end.
 
 Type
   match Niln nat with
-  | Niln => 0
-  | Consn n a Niln => n
-  | Consn n a (Consn m b l) => n + m
+  | Niln _ => 0
+  | Consn _ n a (Niln _) => n
+  | Consn _ n a (Consn _ m b l) => n + m
   end.
 
 
@@ -1027,17 +1017,17 @@ Type
 
 Type
   match LE_n 0 return nat with
-  | LE_n => 0
-  | LE_S m LE_n => 0 + m
-  | LE_S m (LE_S y h) => 0 + m
+  | LE_n _ => 0
+  | LE_S _ m (LE_n _) => 0 + m
+  | LE_S _ m (LE_S _ y h) => 0 + m
   end.
 
 
 Type
   match LE_n 0 with
-  | LE_n => 0
-  | LE_S m LE_n => 0 + m
-  | LE_S m (LE_S y h) => 0 + m
+  | LE_n _ => 0
+  | LE_S _ m (LE_n _) => 0 + m
+  | LE_S _ m (LE_S _ y h) => 0 + m
   end.
 
 
@@ -1077,25 +1067,25 @@ Type
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l return (nat -> nat) with
-   | Niln => fun _ : nat => 0
-   | Consn n a Niln => fun _ : nat => n
-   | Consn n a (Consn m b l) => fun _ : nat => n + m
+   | Niln _ => fun _ : nat => 0
+   | Consn _ n a (Niln _) => fun _ : nat => n
+   | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m
    end).
 
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l with
-   | Niln => fun _ : nat => 0
-   | Consn n a Niln => fun _ : nat => n
-   | Consn n a (Consn m b l) => fun _ : nat => n + m
+   | Niln _ => fun _ : nat => 0
+   | Consn _ n a (Niln _) => fun _ : nat => n
+   | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m
    end).
 
 (* Also tests for multiple _ patterns *)
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l in (Listn _ n) return (Listn A n) with
-   | Niln as b => b
-   | Consn _ _ _ as b => b
+   | Niln _ as b => b
+   | Consn _ _ _ _ as b => b
    end).
 
 (** This one was said to raised once an "Horrible error message!" *)
@@ -1103,8 +1093,8 @@ Type
 Type
   (fun (A:Set) (n:nat) (l:Listn A n) =>
    match l with
-   | Niln as b => b
-   | Consn _ _ _  as b =>  b
+   | Niln _ as b => b
+   | Consn _ _ _ _  as b =>  b
    end).
 
 Type
@@ -1123,26 +1113,26 @@ Type
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h return (nat -> nat) with
-   | LE_n => fun _ : nat => n
-   | LE_S m LE_n => fun _ : nat => n + m
-   | LE_S m (LE_S y h) => fun _ : nat => m + y
+   | LE_n _ => fun _ : nat => n
+   | LE_S _ m (LE_n _) => fun _ : nat => n + m
+   | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y
    end).
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h with
-   | LE_n => fun _ : nat => n
-   | LE_S m LE_n => fun _ : nat => n + m
-   | LE_S m (LE_S y h) => fun _ : nat => m + y
+   | LE_n _ => fun _ : nat => n
+   | LE_S _ m (LE_n _) => fun _ : nat => n + m
+   | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y
    end).
 
 
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h return nat with
-   | LE_n => n
-   | LE_S m LE_n => n + m
-   | LE_S m (LE_S y LE_n) => n + m + y
-   | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y')
+   | LE_n _ => n
+   | LE_S _ m (LE_n _) => n + m
+   | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y
+   | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y')
    end).
 
 
@@ -1150,28 +1140,28 @@ Type
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h with
-   | LE_n => n
-   | LE_S m LE_n => n + m
-   | LE_S m (LE_S y LE_n) => n + m + y
-   | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y')
+   | LE_n _ => n
+   | LE_S _ m (LE_n _) => n + m
+   | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y
+   | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y')
    end).
 
 
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h return nat with
-   | LE_n => n
-   | LE_S m LE_n => n + m
-   | LE_S m (LE_S y h) => n + m + y
+   | LE_n _ => n
+   | LE_S _ m (LE_n _) => n + m
+   | LE_S _ m (LE_S _ y h) => n + m + y
    end).
 
 
 Type
   (fun (n m : nat) (h : LE n m) =>
    match h with
-   | LE_n => n
-   | LE_S m LE_n => n + m
-   | LE_S m (LE_S y h) => n + m + y
+   | LE_n _ => n
+   | LE_S _ m (LE_n _) => n + m
+   | LE_S _ m (LE_S _ y h) => n + m + y
    end).
 
 Type
@@ -1231,14 +1221,14 @@ Parameter B : Set.
 Type
   (fun (P : nat -> B -> Prop) (x : SStream B P) =>
    match x return B with
-   | scons _ a _ _ => a
+   | scons _ _ a _ _ => a
    end).
 
 
 Type
   (fun (P : nat -> B -> Prop) (x : SStream B P) =>
    match x with
-   | scons _ a _ _ => a
+   | scons _ _ a _ _ => a
    end).
 
 Type match (0, 0) return (nat * nat) with
@@ -1267,14 +1257,14 @@ Parameter concat : forall A : Set, List A -> List A -> List A.
 
 Type
   match Nil nat, Nil nat return (List nat) with
-  | Nil as b, x => concat nat b x
-  | Cons _ _ as d, Nil as c => concat nat d c
+  | Nil _ as b, x => concat nat b x
+  | Cons _ _ _ as d, Nil _ as c => concat nat d c
   | _, _ => Nil nat
   end.
 Type
   match Nil nat, Nil nat with
-  | Nil as b, x => concat nat b x
-  | Cons _ _ as d, Nil as c => concat nat d c
+  | Nil _ as b, x => concat nat b x
+  | Cons _ _ _ as d, Nil _ as c => concat nat d c
   | _, _ => Nil nat
   end.
 
@@ -1415,7 +1405,7 @@ Parameter p : eq_prf.
 
 Type
   match p with
-  | ex_intro c eqc =>
+  | ex_intro _ c eqc =>
       match eq_nat_dec c n with
       | right _ => refl_equal n
       | left y => (* c=n*)  refl_equal n
@@ -1438,7 +1428,7 @@ Type
   (fun N : nat =>
    match N_cla N with
    | inright H => match exist_U2 N H with
-                  | exist a b => a
+                  | exist _ a b => a
                   end
    | _ => 0
    end).
@@ -1636,8 +1626,8 @@ Parameter
 
 Type
   match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with
-  | Nil => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat)
-  | Cons a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y)
+  | Nil _ => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat)
+  | Cons _ a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y)
   end.
 
 
@@ -1687,20 +1677,20 @@ Parameter
 
 Type
   match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
-  | Nil, Nil => V1
-  | Nil, Cons a x => V2 a x
-  | Cons a x, Nil => V3 a x
-  | Cons a x, Cons b y => V4 a x b y
+  | Nil _, Nil _ => V1
+  | Nil _, Cons _ a x => V2 a x
+  | Cons _ a x, Nil _ => V3 a x
+  | Cons _ a x, Cons _ b y => V4 a x b y
   end.
 
 
 Type
   (fun x y : List nat =>
    match x, y return (eqlong x y \/ ~ eqlong x y) with
-   | Nil, Nil => V1
-   | Nil, Cons a x => V2 a x
-   | Cons a x, Nil => V3 a x
-   | Cons a x, Cons b y => V4 a x b y
+   | Nil _, Nil _ => V1
+   | Nil _, Cons _ a x => V2 a x
+   | Cons _ a x, Nil _ => V3 a x
+   | Cons _ a x, Cons _ b y => V4 a x b y
    end).
 
 
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index bfead53c0a..8d9edbd62d 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -4,8 +4,8 @@ Check
   (fun (P : nat -> Prop) Q (A : P 0 -> Q) (B : forall n : nat, P (S n) -> Q)
      x =>
    match x return Q with
-   | exist O H => A H
-   | exist (S n) H => B n H
+   | exist _ O H => A H
+   | exist _ (S n) H => B n H
    end).
 
 (* Check dependencies in anonymous arguments (from FTA/listn.v) *)
@@ -21,30 +21,30 @@ Variable c : C.
 
 Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
   match bs with
-  | niln => c
-  | consn b _ tl => g b (foldrn _ tl)
+  | niln _ => c
+  | consn _ b _ tl => g b (foldrn _ tl)
   end.
 End Folding.
 
 (** Testing post-processing of nested dependencies *)
 
 Check fun x:{x|x=0}*nat+nat => match x with
-      | inl ((exist 0 eq_refl),0) => None
+      | inl ((exist _ 0 eq_refl),0) => None
       | _ => Some 0
       end.
 
 Check fun x:{_:{x|x=0}|True}+nat => match x with
-      | inl (exist (exist 0 eq_refl) I) => None
+      | inl (exist _ (exist _ 0 eq_refl) I) => None
       | _ => Some 0
       end.
 
 Check fun x:{_:{x|x=0}|True}+nat => match x with
-      | inl (exist (exist 0 eq_refl) I) => None
+      | inl (exist _ (exist _ 0 eq_refl) I) => None
       | _ => Some 0
       end.
 
 Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
-      | inl (exist (exist 0 eq_refl) I) => None
+      | inl (exist _ (exist _ 0 eq_refl) I) => None
       | _ => Some 0
       end.
 
@@ -52,11 +52,11 @@ Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
   (* due to a bug in dependencies postprocessing (revealed by CoLoR) *)
 
 Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with
-      | exist2 (x,y) eq_refl I => None
+      | exist2 _ _ (x,y) eq_refl I => None
       end.
 
 Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with
-      | inl (exist (exist2 (x,y) eq_refl I) I) => None
+      | inl (exist _ (exist2 _ _ (x,y) eq_refl I) I) => None
       | _ => Some 0
       end.
 
@@ -521,8 +521,8 @@ end.
 
 Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) :=
   match v with
-    | niln => w
-    | consn a n' v' => consn _ a _ (app v' w)
+    | niln _ => w
+    | consn _ a n' v' => consn _ a _ (app v' w)
   end.
 
 (* Testing regression of bug 2106 *)
@@ -547,7 +547,7 @@ n'.
 
 Definition test (s:step E E) :=
   match s with
-    | Step nil _ (cons E nil) _ Plus l l' => true
+    | @Step nil _ (cons E nil) _ Plus l l' => true
     | _ => false
   end.
 
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 3a4f88993f..5fc703cf0f 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -42,8 +42,8 @@ Variables (B C : Set) (g : B -> C -> C) (c : C).
 
 Fixpoint foldrn n bs :=
   match bs with
-  | Vnil => c
-  | Vcons b _ tl => g b (foldrn _ tl)
+  | Vnil _ => c
+  | Vcons _ b _ tl => g b (foldrn _ tl)
   end.
 
 End folding.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index 84ec298df9..a654080de8 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -9,11 +9,11 @@ Require Import Coq.Program.Program.
 Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n :=
   match v with
     | vnil => !
-    | vcons a n' v' => v'
+    | vcons a v' => v'
   end.
 
 Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) :=
   match v in vector _ n return vector A (n + m) with
     | vnil => w
-    | vcons a n' v' => vcons a (app v' w)
+    | vcons a v' => vcons a (app v' w)
   end.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 59aa87de4e..5e59930f3b 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -38,7 +38,7 @@ Check
      (f : forall z : C, P z (I C D x y z)) (y0 : C)
      (a : A C D x y y0) =>
    match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
-   | I x0 => f x0
+   | I _ _ _ _ x0 => f x0
    end).
 
 Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set :=  {p : C; q : E}.
@@ -51,7 +51,7 @@ Check
      (f : forall p0 q0 : C, P (Build_B C D x y p0 q0))
      (b : B C D x y) =>
    match b as b0 return (P b0) with
-   | Build_B x0 x1 => f x0 x1
+   | Build_B _ _ _ _ x0 x1 => f x0 x1
    end).
 
 (* Check inductive types with local definitions (constructors) *)
diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
index 4c790680d6..0e557aee07 100644
--- a/test-suite/success/LetPat.v
+++ b/test-suite/success/LetPat.v
@@ -9,22 +9,22 @@ Print l3.
 
 Record someT (A : Type) := mkT { a : nat; b: A }.
 
-Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x.
+Definition l4 A (t : someT A) : nat := let 'mkT _ x y := t in x.
 Print l4.
 Print sigT.
 
 Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
-  let 'existT x y := t return B (projT1 t) in y.
+  let 'existT _ x y := t return B (projT1 t) in y.
 
 Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
-  let 'existT x y as t' := t return B (projT1 t') in y.
+  let 'existT _ x y as t' := t return B (projT1 t') in y.
 
 Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
-  let 'existT x y as t' in sigT _ := t return B (projT1 t') in y.
+  let 'existT _ x y as t' in sigT _ := t return B (projT1 t') in y.
 
 Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
   match t with
-    existT x y => y
+    existT _ x y => y
   end.
 
 (** An example from algebra, using let' and inference of return clauses
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 459645f6f8..15af084424 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -301,8 +301,8 @@ Section Le_case_analysis.
            (HS : forall m, n <= m -> Q (S m)).
  Check (
     match H in (_ <= q) return (Q q)  with
-    | le_n => H0
-    | le_S m Hm => HS m Hm
+    | le_n _ => H0
+    | le_S _ m Hm => HS m Hm
     end
   ).
 
@@ -320,8 +320,8 @@ Qed.
 Definition Vtail_total
    (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
 match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
-| Vector.nil => Vector.nil A
-| Vector.cons _ n0 v0 => v0
+| Vector.nil _ => Vector.nil A
+| Vector.cons _ _ n0 v0 => v0
 end.
 
 Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
@@ -1060,8 +1060,8 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
                   : option A :=
   match n,v  with
     _   , Vector.nil => None
-  | 0   , Vector.cons b  _ _ => Some b
-  | S n', Vector.cons _  p' v' => vector_nth A n'  p' v'
+  | 0   , Vector.cons b _ => Some b
+  | S n', Vector.cons _ v' => vector_nth A n' _ v'
   end.
 
 Implicit Arguments vector_nth [A p].
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 4292ecb6ad..b538d2ed27 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -96,13 +96,13 @@ Inductive list (A : Type) : Type :=
   nil : list A | cons : A -> list A -> list A.
 Inductive vect (A : Type) : nat -> Type :=
   vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n).
-Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end.
+Fixpoint size A (l : list A) : nat := match l with nil _ => 0 | cons _ _ tl => 1+size _ tl end.
 
 Section test_non_unif_but_complete.
 Fixpoint l2v A (l : list A) : vect A (size A l) :=
   match l as l return vect A (size A l) with
-  | nil => vnil A
-  | cons x xs => vcons A (size A xs) x (l2v A xs)
+  | nil _ => vnil A
+  | cons _ x xs => vcons A (size A xs) x (l2v A xs)
   end.
 
 Local Coercion l2v : list >-> vect.
@@ -121,8 +121,8 @@ Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C)
 
 Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := 
   match l as l return vect B (size A l) with
-  | nil => vnil B
-  | cons x xs => vcons _ _ (c x) (l2v2 xs) end.
+  | nil _ => vnil B
+  | cons _ x xs => vcons _ _ (c x) (l2v2 xs) end.
 
 Local Coercion l2v2 : list >-> vect.
 
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ff8b28baea..0e7d653b4f 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -51,7 +51,7 @@ Check
   (let p :=
      fun (m : nat) f (n : nat) =>
      match f m n with
-     | exist a b => exist _ a b
+     | exist _ a b => exist _ a b
      end in
    p
    :forall x : nat,
@@ -178,9 +178,9 @@ refine
        | left _ => _
        | right _ =>
            match le_step s _ _ with
-           | exist s' h' =>
+           | exist _ s' h' =>
                match hr s' _ _ with
-               | exist s'' _ => exist _ s'' _
+               | exist _ s'' _ => exist _ s'' _
                end
            end
        end)).
@@ -204,7 +204,7 @@ Abort.
 Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) :=
   match l with
   | nil => nil
-  | (existT k v)::l' => (existT _ k v):: (filter A l')
+  | (existT _ k v)::l' => (existT _ k v):: (filter A l')
   end.
 
 (* Bug #2000: used to raise Out of memory in 8.2 while it should fail by
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 8b4f410550..352abb2af5 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -84,7 +84,7 @@ Definition div :
 refine
   (fun m div_rec n =>
      match div_rec m n with
-     | exist _ _ => _
+     | exist _ _ _ => _
      end).
 Abort.