Unset Asymmetric Patterns

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

4 files changed, 13 insertions, 13 deletions

diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 792e2c3c2c..c580ba75b2 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 fccacc742f..018b5c83fa 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 440070a15a..046c1b7cf8 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 bdc4671df9..d8ab6fd30d 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)