Unset Asymmetric Patterns

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

29 files changed, 255 insertions, 243 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
index 947d15f0d2..884ac01cd2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1834.v
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -53,7 +53,7 @@ Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
    y1 e1.
 
 Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
-  match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+  match E with exist _ e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
 
 Definition eq_2 y0 y1 y2 :=
   {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
@@ -81,7 +81,7 @@ Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y2 e2.
 
 Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
-  match E with exist (exist e0 e1) e2 =>
+  match E with exist _ (exist _ e0 e1) e2 =>
      S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
 
 Definition eq_3 y0 y1 y2 y3 :=
@@ -118,7 +118,7 @@ Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y3 e3.
 
 Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
-  match E with exist (exist (exist e0 e1) e2) e3 =>
+  match E with exist _ (exist _ (exist _ e0 e1) e2) e3 =>
      S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
 
 Definition eq_4 y0 y1 y2 y3 y4 :=
@@ -165,7 +165,7 @@ Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
    y4 e4.
 
 Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
-  match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+  match E with exist _ (exist _ (exist _ (exist _ e0 e1) e2) e3) e4 =>
      S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
 
 Definition eq_5 y0 y1 y2 y3 y4 y5 :=
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 2d90a2f1dc..685811176a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
-    refine (match x return _ with mkT n => fun g => f (g _) end).
+    refine (match x return _ with mkT _ n => fun g => f (g _) end).
     trivial.
   Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2353.v b/test-suite/bugs/closed/shouldsucceed/2353.v
index b5c45c28c7..baae9a6ece 100644
--- a/test-suite/bugs/closed/shouldsucceed/2353.v
+++ b/test-suite/bugs/closed/shouldsucceed/2353.v
@@ -4,9 +4,9 @@ Inductive term n := app (l : list term n).
 Definition term_list :=
   fix term_size n (t : term n) (acc : nat) {struct t} : nat :=
     match t with
-    | app l =>
+    | app _ l =>
       (fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat :=
       match l with
-      | cons t q => term_list_size (S n) q (term_size n t acc)
+      | cons _ _ t q => term_list_size (S n) q (term_size n t acc)
       end) n l (S acc)
     end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
index 7deec64dd0..ab39633f87 100644
--- a/test-suite/bugs/closed/shouldsucceed/2378.v
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -66,9 +66,9 @@ Implicit Arguments lpSat.
 
 Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   match f with
-    LPPred p => p2lp p
-  | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
-  | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+    LPPred _ p => p2lp p
+  | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+  | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
   end.
 Implicit Arguments LPTransfo.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
index fe8eba5496..8ac696e912 100644
--- a/test-suite/bugs/closed/shouldsucceed/2404.v
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -37,8 +37,8 @@ Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
 
 Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
   match aRWb,y with
-  | starReflS a, y' => Some y'
-  | starTransS i j k jWk jRWi, y' =>
+  | starReflS _ a, y' => Some y'
+  | starTransS jWk jRWi, y' =>
     match (bexportw jWk y) with
     | Some x => exportRweak jRWi x
     | None   => None
diff --git a/test-suite/bugs/closed/shouldsucceed/2729.v b/test-suite/bugs/closed/shouldsucceed/2729.v
index 44f8d3c7c9..3efca5d993 100644
--- a/test-suite/bugs/closed/shouldsucceed/2729.v
+++ b/test-suite/bugs/closed/shouldsucceed/2729.v
@@ -53,12 +53,12 @@ Program Fixpoint insertBase {pu : PatchUniverse}
                             (qs : SequenceBase pu mid to)
                           : SequenceBase pu from to
     := match qs with
-       | Nil _ => Cons p Nil
-       | Cons mid' mid2' to' q qs' =>
+       | Nil => Cons p Nil
+       | Cons q qs' =>
            match SignedName_compare (pu_nameOf p) (pu_nameOf q) with
            | Lt => Cons p qs
            | _  => match commutable_dec p (castPatchFrom _ q) with
-                   | inleft (existT _ (existT q' (existT p' _))) => Cons q'
+                   | inleft (existT _ _ (existT _ q' (existT _ p' _))) => Cons q'
 (insertBase p' qs')
                    | inright _ => Cons p qs
                    end
diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v
index 1845dd1f60..a0668cd19b 100644
--- a/test-suite/bugs/opened/shouldnotfail/1501.v
+++ b/test-suite/bugs/opened/shouldnotfail/1501.v
@@ -40,11 +40,13 @@ Parameter
 
 Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
 
-Add Relation K equiv
- reflexivity proved by (@equiv_refl)
- symmetry proved by (@equiv_sym)
- transitivity proved by (@equiv_trans)
- as equiv_rel.
+Instance equiv_rel A: Equivalence (@equiv A).
+Proof.
+ constructor.
+ intros xa; apply equiv_refl.
+ intros xa xb; apply equiv_sym.
+ intros xa xb xc; apply equiv_trans.
+Defined.
 
 Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
 x)).
@@ -67,17 +69,17 @@ Proof.
   unfold fequiv; intros; eapply equiv_trans; auto with monad.
 Qed.
 
-Add Relation (fun (A B:Type) => A -> K B) fequiv
- reflexivity proved by (@fequiv_refl)
- symmetry proved by (@fequiv_sym)
- transitivity proved by (@fequiv_trans)
- as fequiv_rel.
+Instance fequiv_re A B: Equivalence (@fequiv A B).
+Proof.
+ constructor.
+ intros f; apply fequiv_refl.
+ intros f g; apply fequiv_sym.
+ intros f g h; apply fequiv_trans.
+Defined.
 
-Add Morphism bind
- with signature equiv ==> fequiv ==> equiv
- as bind_mor.
+Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B).
 Proof.
- unfold fequiv; intros; apply bind_compat; auto.
+ unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto.
 Qed.
 
 Lemma test:
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
index de77e35d32..22f61ab727 100644
--- a/test-suite/bugs/opened/shouldnotfail/1596.v
+++ b/test-suite/bugs/opened/shouldnotfail/1596.v
@@ -100,6 +100,16 @@ Definition t := (X.t * Y.t)%type.
     left;trivial.
   Defined.
 
+  Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
+  Proof.
+    intros [xa xb] [ya yb]; simpl.
+    destruct (X.eq_dec xa ya).
+    destruct (Y.eq_dec xb yb).
+    + left; now split.
+    + right. now intros [eqa eqb].
+    + right. now intros [eqa eqb].
+  Defined.
+
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
 End OrderedPair.
@@ -158,6 +168,14 @@ GT;simpl;trivial;fail).
       apply GT;trivial.
     Defined.
 
+    Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
+    Proof.
+    intros [i] [j]. unfold eq.
+    destruct (eq_nat_dec i j).
+    + left. now f_equal.
+    + right. intros meq; now inversion meq.
+    Defined.
+
     Hint Immediate eq_sym.
     Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
   End Ord.
diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v
index d63c49403b..ec48523009 100644
--- a/test-suite/failure/Case9.v
+++ b/test-suite/failure/Case9.v
@@ -2,7 +2,9 @@ Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
 Type
   match compare 0 0 return nat with
 
-      (* k<i *) | left _ _ (left _ _ _) => 0
-   (* k=i *) | left _ _ _ => 0
-   (* k>i *) | right _ _ _ => 0
+      (* k<i *) | left _ (left _ _) => 0
+   (* k=i *) | left _ _ => 0
+   (* k>i *) | right _ _ => 0
+  end.
+
   end.
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 324dc60301..cd3c81f493 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -5,9 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-
+(*
 Fixpoint F (n:nat) : False := F (match F n with end).
-
+*)
 (* de Bruijn mix-up *)
 (* If accepted, Eval compute in f 0. loops *)
 Definition f :=
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 341805a16b..7214287a6a 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -145,8 +145,8 @@ Module ListDict (E: ELEM).
   Definition add (e : elt) (s : T) := cons elt e s.
   Fixpoint find (e : elt) (s : T) {struct s} : bool :=
     match s with
-    | nil => false
-    | cons e' s' => ifte (E.eq_dec e e') true (find e s')
+    | nil _ => false
+    | cons _ e' s' => ifte (E.eq_dec e e') true (find e s')
     end.
 
   Definition find_empty_false (e : elt) := refl_equal false.
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index f5610efc41..6c514b16ee 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -22,8 +22,8 @@ Inductive hole (A:Set) : Set := Hole | Hole2.
 
 Definition wrong_id (A B : Set) (x:hole A) : hole B :=
  match x with
-  | Hole => @Hole _
-  | Hole2 => @Hole2 _
+  | Hole _ => @Hole _
+  | Hole2 _ => @Hole2 _
  end.
 
 Extraction wrong_id. (** should _not_ be optimized as an identity *)
@@ -114,9 +114,9 @@ Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode)
     | Some oc =>
       match f w with
         | DecInst i => DecInst (g i oc)
-        | DecError m => @DecError inst m
-        | DecUndefined => @DecUndefined inst
-        | DecUnpredictable => @DecUnpredictable inst
+        | DecError _ m => @DecError inst m
+        | DecUndefined _ => @DecUndefined inst
+        | DecUnpredictable _ => @DecUnpredictable inst
       end
     | None => @DecUndefined inst
   end.
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.