Unset Asymmetric Patterns

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

50 files changed, 348 insertions, 336 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7f6f5672b..449979162 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -19,7 +19,7 @@ open Constrexpr_ops
 (*i*)
 
 
-let oldfashion_patterns = ref (true)
+let oldfashion_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
   Goptions.optname =
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 792e2c3c2..c580ba75b 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -66,7 +66,7 @@ Require Import EnvRing.
 Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
   match e with
     | PEc c =>  c
-    | PEX j =>  env j
+    | PEX _ j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
@@ -78,7 +78,7 @@ Lemma Qeval_expr_simpl : forall env e,
   Qeval_expr env e =
   match e with
     | PEc c =>  c
-    | PEX j =>  env j
+    | PEX _ j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index fccacc742..018b5c83f 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -947,7 +947,7 @@ Variable phi_C_of_S :   forall c,  phiS c =  phi (C_of_S c).
 Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
   match e with
     | PEc c => PEc (C_of_S c)
-    | PEX p => PEX _ p
+    | PEX _ p => PEX _ p
     | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
     | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
     | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 440070a15..046c1b7cf 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -31,10 +31,10 @@ Set Implicit Arguments.
 
   Fixpoint eval_f (A:Type)  (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop :=
     match f with
-      | TT => True
-      | FF => False
+      | TT _ => True
+      | FF _ => False
       | A a =>  ev a
-      | X p => p
+      | X _ p => p
       | Cj e1 e2 => (eval_f  ev e1) /\ (eval_f ev e2)
       | D e1 e2  => (eval_f  ev e1) \/ (eval_f  ev e2)
       | N e     => ~ (eval_f  ev e)
@@ -54,9 +54,9 @@ Set Implicit Arguments.
 
   Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U :=
     match f with
-      | TT => TT _
-      | FF => FF _
-      | X p => X _ p
+      | TT _ => TT _
+      | FF _ => FF _
+      | X _ p => X _ p
       | A a => A (fct a)
       | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2)
       | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2)
@@ -172,9 +172,9 @@ Set Implicit Arguments.
 
     Fixpoint xcnf (pol : bool) (f : BFormula Term)  {struct f}: cnf :=
       match f with
-        | TT => if pol then tt else ff
-        | FF => if pol then ff else tt
-        | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *)
+        | TT _ => if pol then tt else ff
+        | FF _ => if pol then ff else tt
+        | X _ p => if pol then ff else ff (* This is not complete - cannot negate any proposition *)
         | A x => if pol then normalise x else negate x
         | N e  => xcnf (negb pol) e
         | Cj e1 e2 =>
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index bdc4671df..d8ab6fd30 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -62,7 +62,7 @@ Qed.
 Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
   match e with
     | PEc c => c
-    | PEX x => env x
+    | PEX _ x => env x
     | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
     | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
     | PEpow e1 n  => Z.pow (Zeval_expr env e1) (Z.of_N n)
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 4f4f20396..5c1f4c470 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -241,7 +241,7 @@ Fixpoint interpret3 t fv {struct t}: R :=
   | (PEpow t1 t2) =>
        let v1  := interpret3 t1 fv in pow v1 (N.to_nat t2)
   | (PEc t1) => (IZR1 t1)
-  | (PEX n) => List.nth (pred (Pos.to_nat n)) fv 0
+  | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0
   end.
 
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 341c0e6f5..2f30b6e17 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -407,7 +407,7 @@ Qed.
 Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
  match e1, e2 with
    PEc c1, PEc c2 => ceqb c1 c2
-  | PEX p1, PEX p2 => Pos.eqb p1 p2
+  | PEX _ p1, PEX _ p2 => Pos.eqb p1 p2
   | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
   | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
   | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 24c92b57f..7ffe98e29 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -419,7 +419,7 @@ Qed.
  Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
    match pe with
    | PEc c => [c]
-   | PEX j => nth 0 j l
+   | PEX _ j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
    | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
    | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
@@ -501,7 +501,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Fixpoint norm_aux (pe:PExpr C) : Pol :=
    match pe with
    | PEc c => Pc c
-   | PEX j => mk_X j
+   | PEX _ j => mk_X j
    | PEadd pe1 (PEopp pe2) =>
      Psub (norm_aux pe1) (norm_aux pe2)
    | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
index 947d15f0d..884ac01cd 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 2d90a2f1d..685811176 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 b5c45c28c..baae9a6ec 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 7deec64dd..ab39633f8 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 fe8eba549..8ac696e91 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 44f8d3c7c..3efca5d99 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 1845dd1f6..a0668cd19 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 de77e35d3..22f61ab72 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 d63c49403..ec4852300 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 324dc6030..cd3c81f49 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 341805a16..7214287a6 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 f5610efc4..6c514b16e 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 c8f772687..445ffac8c 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 729ab824f..55e17facc 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 77016bbfe..ce9a0ecb4 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 66af9e0d3..861d04668 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 6e4b20031..f95598aad 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 a8534a0b9..e34e5b9ba 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 543ca0c92..cf102486a 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 c9a3c08ef..257c55fd8 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 bfead53c0..8d9edbd62 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 3a4f88993..5fc703cf0 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 84ec298df..a654080de 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 59aa87de4..5e59930f3 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 4c790680d..0e557aee0 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 459645f6f..15af08442 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 4292ecb6a..b538d2ed2 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 ff8b28bae..0e7d653b4 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 8b4f41055..352abb2af 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.
 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index e0bed0d37..9b8ebfe55 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -38,15 +38,15 @@ Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
 Proof.
 fix 3.
 refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
-  with le_n => _ |le_S i H => _ end).
+  with le_n _ => _ |le_S _ i H => _ end).
 refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, 
   le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
-    |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl).
+    |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl).
 rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
 subst m. destruct (Lt.lt_irrefl j H').
 refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
   with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
-    with |le_n => _ |le_S j H2 => fun H' => _ end H).
+    with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H).
 destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
 f_equal. apply le_unique.
 Qed.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f42f1e9e0..5d34a4bf5 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -342,7 +342,7 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
 
 Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _   => Leaf _
    | Node l x d r h => Node (map f l) x (f d) (map f r) h
   end.
 
@@ -350,7 +350,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
 
 Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
   match m with
-   | Leaf   => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
   end.
 
@@ -359,7 +359,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
 Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
   : t elt' :=
   match m with
-   | Leaf => Leaf _
+   | Leaf _ => Leaf _
    | Node l x d r h =>
       match f x d with
        | Some d' => join (map_option f l) x d' (map_option f r)
@@ -389,8 +389,8 @@ Variable mapr : t elt' -> t elt''.
 
 Fixpoint map2_opt m1 m2 :=
  match m1, m2 with
-  | Leaf, _ => mapr m2
-  | _, Leaf => mapl m1
+  | Leaf _, _ => mapr m2
+  | _, Leaf _ => mapl m1
   | Node l1 x1 d1 r1 h1, _ =>
      let (l2',o2,r2') := split x1 m2 in
      match f x1 d1 o2 with
@@ -1424,7 +1424,7 @@ Qed.
     i.e. the list of elements actually compared *)
 
 Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
-  | End => nil
+  | End _ => nil
   | More x e t r => (x,e) :: elements t ++ flatten_e r
  end.
 
@@ -2016,7 +2016,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
    match e2 with
-    | R.End => Gt
+    | R.End _ => Gt
     | R.More x2 d2 r2 e2 =>
        match X.compare x1 x2 with
         | EQ _ => match D.compare d1 d2 with
@@ -2033,7 +2033,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
    match s1 with
-    | R.Leaf => cont e2
+    | R.Leaf _ => cont e2
     | R.Node l1 x1 d1 r1 _ =>
        compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
    end.
@@ -2041,7 +2041,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   (** Initial continuation *)
 
   Definition compare_end (e2:R.enumeration D.t) :=
-   match e2 with R.End => Eq | _ => Lt end.
+   match e2 with R.End _ => Eq | _ => Lt end.
 
   (** The complete comparison *)
 
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index e1c603514..59b778369 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
     match e with
-     | Raw.End => 0%nat
+     | Raw.End _ => 0%nat
      | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
     end.
 
@@ -677,9 +677,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
    { measure cardinal_e_2 ee } : comparison :=
   match ee with
-  | (Raw.End, Raw.End) => Eq
-  | (Raw.End, Raw.More _ _ _ _) => Lt
-  | (Raw.More _ _ _ _, Raw.End) => Gt
+  | (Raw.End _, Raw.End _) => Eq
+  | (Raw.End _, Raw.More _ _ _ _) => Lt
+  | (Raw.More _ _ _ _, Raw.End _) => Gt
   | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
       match X.compare x1 x2 with
       | EQ _ => match D.compare d1 d2 with
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index d562245d8..5e968d4d3 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -902,7 +902,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
     Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
       match m with
-        | Leaf => v
+        | Leaf _ => v
         | Node l (Some x) r =>
           xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
         | Node l None r =>
@@ -940,8 +940,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool :=
     match m1, m2 with
-      | Leaf, _ => is_empty m2
-      | _, Leaf => is_empty m1
+      | Leaf _, _ => is_empty m2
+      | _, Leaf _ => is_empty m1
       | Node l1 o1 r1, Node l2 o2 r2 =>
            (match o1, o2 with
              | None, None => true
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 1ac544e1f..6aebcf501 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
 
   Lemma choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _                        => False
      end.
@@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition choose (s : t) : option elt :=
     match choose s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition min_elt (s : t) : option elt :=
     match min_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
@@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition max_elt (s : t) : option elt :=
     match max_elt s with
-    | inleft (exist x _) => Some x
+    | inleft (exist _ x _) => Some x
     | inright _ => None
     end.
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a03611193..c791f49a6 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -497,7 +497,7 @@ Module Type Sdep.
         in the dependent version of [choose], so we leave it separate. *)
   Parameter choose_equal : forall s s', Equal s s' ->
      match choose s, choose s' with
-       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
        | inright _, inright _  => True
        | _, _  => False
      end.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1610f0a1..6adc1c369 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -72,12 +72,12 @@ Section Subset_projections.
   Variable P : A -> Prop.
 
   Definition proj1_sig (e:sig P) := match e with
-                                    | exist a b => a
+                                    | exist _ a b => a
                                     end.
 
   Definition proj2_sig (e:sig P) :=
     match e return P (proj1_sig e) with
-    | exist a b => b
+    | exist _ a b => b
     end.
 
 End Subset_projections.
@@ -96,11 +96,11 @@ Section Projections.
   Variable P : A -> Type.
 
   Definition projT1 (x:sigT P) : A := match x with
-                                      | existT a _ => a
+                                      | existT _ a _ => a
                                       end.
   Definition projT2 (x:sigT P) : P (projT1 x) :=
     match x return P (projT1 x) with
-    | existT _ h => h
+    | existT _ _ h => h
     end.
 
 End Projections.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index ea5b16517..9bde2d641 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -101,7 +101,7 @@ Section EqdepDec.
 
   Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
     match exP with
-      | ex_intro x' prf =>
+      | ex_intro _ x' prf =>
         match eq_dec x' x with
           | or_introl eqprf => eq_ind x' P prf x eqprf
           | _ => def
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index b50adaab8..662c50abf 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -512,9 +512,9 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
 
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
-    | Vector.nil => N0
-    | Vector.cons false n bv => N.double (Bv2N n bv)
-    | Vector.cons true n bv => N.succ_double (Bv2N n bv)
+    | Vector.nil _ => N0
+    | Vector.cons _ false n bv => N.double (Bv2N n bv)
+    | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
   end.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d523a1f44..9de60bb5d 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -144,7 +144,7 @@ Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f).
 
 Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
   match projT2 (pre f) with
-    | existT a b => a
+    | existT _ a b => a
   end.
 
 Fixpoint Int_SF (l k:Rlist) : R :=
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index ae33e6318..b6ec6307c 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -23,14 +23,14 @@ Inductive t : nat -> Set :=
 
 Section SCHEMES.
 Definition case0 P (p: t 0): P p :=
-  match p with | F1 _ | FS _ _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
+  match p with | F1 | FS  _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
 
 Definition caseS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
   {n} (p: t (S n)): P p :=
   match p with
-  |F1 k => P1 k
-  |FS k pp => PS pp
+  |@F1 k => P1 k
+  |FS pp => PS pp
   end.
 
 Definition rectS (P: forall {n}, t (S n) -> Type)
@@ -38,9 +38,9 @@ Definition rectS (P: forall {n}, t (S n) -> Type)
   forall {n} (p: t (S n)), P p :=
 fix rectS_fix {n} (p: t (S n)): P p:=
   match p with
-  |F1 k => P1 k
-  |FS 0 pp => case0 (fun f => P (FS f)) pp
-  |FS (S k) pp => PS pp (rectS_fix pp)
+  |@F1 k => P1 k
+  |@FS 0 pp => case0 (fun f => P (FS f)) pp
+  |@FS (S k) pp => PS pp (rectS_fix pp)
   end.
 
 Definition rect2 (P: forall {n} (a b: t n), Type)
@@ -51,14 +51,14 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
     forall {n} (a b: t n), P a b :=
 fix rect2_fix {n} (a: t n): forall (b: t n), P a b :=
 match a with
-  |F1 m => fun (b: t (S m)) => match b as b' in t (S n')
+  |@F1 m => fun (b: t (S m)) => match b as b' in t (S n')
                    return P F1 b' with
-                     |F1 m' => H0 m'
-                     |FS m' b' => H1 b'
+                     |@F1 m' => H0 m'
+                     |FS b' => H1 b'
                    end
-  |FS m a' => fun (b: t (S m)) => match b with
-                         |F1 m' => fun aa: t m' => H2 aa
-                         |FS m' b' => fun aa: t m' => HS aa b' (rect2_fix aa b')
+  |@FS m a' => fun (b: t (S m)) => match b with
+                         |@F1 m' => fun aa: t m' => H2 aa
+                         |FS b' => fun aa => HS aa b' (rect2_fix aa b')
                        end a'
 end.
 End SCHEMES.
@@ -66,15 +66,15 @@ End SCHEMES.
 Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
 match eq in _ = a return
   match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
-  with @F1 _ =>  fun _ => True |@FS _ y => fun x' => x' = y end x with
+  with F1 =>  fun _ => True |FS y => fun x' => x' = y end x with
   eq_refl => eq_refl
 end.
 
 (** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
 Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
   match n with
-    |F1 j => exist _ 0 (Lt.lt_0_Sn j)
-    |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
+    |@F1 j => exist _ 0 (Lt.lt_0_Sn j)
+    |FS p => match to_nat p with |exist _ i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
   end.
 
 (** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of
@@ -86,7 +86,7 @@ Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
       |0 => inleft _ (F1)
       |S p' => match of_nat p' n' with
         |inleft f => inleft _ (FS f)
-        |inright arg => inright _ (match arg with |ex_intro m e =>
+        |inright arg => inright _ (match arg with |ex_intro _ m e =>
           ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
       end
     end
@@ -118,15 +118,15 @@ Fixpoint weak {m}{n} p (f : t m -> t n) :
 match p as p' return t (p' + m) -> t (p' + n) with
   |0 => f
   |S p' => fun x => match x with
-     |F1 n' => fun eq : n' = p' + m => F1
-     |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
+     |@F1 n' => fun eq : n' = p' + m => F1
+     |@FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
   end (eq_refl _)
 end.
 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (m + n)] *)
 Fixpoint L {m} n (p : t m) : t (m + n) :=
-  match p with |F1 _ => F1 |FS _ p' => FS (L n p') end.
+  match p with |F1 => F1 |FS p' => FS (L n p') end.
 
 Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
 Proof.
@@ -144,8 +144,8 @@ induction n.
   exact p.
   exact ((fix LS k (p: t k) :=
     match p with
-      |F1 k' => @F1 (S k')
-      |FS _ p' => FS (LS _ p')
+      |@F1 k' => @F1 (S k')
+      |FS p' => FS (LS _ p')
     end) _ IHn).
 Defined.
 
@@ -163,8 +163,8 @@ Qed.
 
 Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
 match o with
-  |F1 m' => L (m' * n) p
-  |FS m' o' => R n (depair o' p)
+  |@F1 m' => L (m' * n) p
+  |FS o' => R n (depair o' p)
 end.
 
 Lemma depair_sanity {m n} (o : t m) (p : t n) :
@@ -181,9 +181,9 @@ Qed.
 Fixpoint eqb {m n} (p : t m) (q : t n) :=
 match p, q with
 | @F1 m', @F1 n' => EqNat.beq_nat m' n'
-| @FS _ _, @F1 _ => false
-| @F1 _, @FS _ _ => false
-| @FS _ p', @FS _ q' => eqb p' q'
+| FS _, F1 => false
+| F1, FS _ => false
+| FS p', FS q' => eqb p' q'
 end.
 
 Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
@@ -219,11 +219,11 @@ Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
 Proof.
 refine (fix cast {m} (v: t m) {struct v} :=
  match v in t m' return forall n, m' = n -> t n with
- |@F1 _ => fun n => match n with
+ |F1 => fun n => match n with
    | 0 => fun H => False_rect _ _
    | S n' => fun H => F1
  end
- |@FS _ f => fun n => match n with
+ |FS f => fun n => match n with
    | 0 => fun H => False_rect _ _
    | S n' => fun H => FS (cast f n' (f_equal pred H))
  end
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 30a8c5699..64c69ba24 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,12 +40,12 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
- |cons a 0 v =>
+ |@cons _ a 0 v =>
    match v with
-     |nil => bas a
+     |nil _ => bas a
      |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
    end
- |cons a (S nn') v => rect a v (rectS_fix v)
+ |@cons _ a (S nn') v => rect a v (rectS_fix v)
  |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
  end.
 
@@ -109,8 +109,8 @@ ocaml function. *)
 Definition nth {A} := 
 fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
- |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
- |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
+ |Fin.F1 => fun v => caseS (fun n v' => A) (fun h n t => h) v
+ |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
    (fun h n t p0 => nth_fix t p0) v) p'
 end v'.
 
@@ -121,8 +121,8 @@ Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
 (** Put [a] at the p{^ th} place of [v] *)
 Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
   match p with
-  |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
-  |Fin.FS k p' => fun v' =>
+  |@Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
+  |Fin.FS p' => fun v' =>
     (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) v') p'
   end v.
 
@@ -251,7 +251,7 @@ match v in t _ n0 return t C n0 -> A with
     |[] => a
     |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
   end
-  |cons vh vn vt => fun w => match w with
+  |@cons _ vh vn vt => fun w => match w with
     |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt
     |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
   end vt
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index a6c832412..9e8d9372c 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -53,7 +53,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
 	| xI xH => c_sqrt 3 1 2 _ _
 	| xO (xO p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r') with
 		| left Hle =>
                   c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1)
@@ -63,7 +63,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xO (xI p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with
 		| left Hle =>
                   c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1)
@@ -74,7 +74,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xI (xO p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with
 		| left Hle =>
                   c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1)
@@ -85,7 +85,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xI (xI p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with
 		| left Hle =>
                   c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1)
@@ -114,7 +114,7 @@ Definition Zsqrt :
 	| Zpos p =>
           fun h =>
             match sqrtrempos p with
-              | c_sqrt s r Heq Hint =>
+              | c_sqrt _ s r Heq Hint =>
 		existT
                 (fun s:Z =>
                   {r : Z |
@@ -150,7 +150,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
   match x with
     | Zpos p =>
       match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with
-	| existT s _ => s
+	| existT _ s _ => s
       end
     | Zneg p => 0
     | Z0 => 0