Unset Asymmetric Patterns

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

7 files changed, 17 insertions, 17 deletions

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)