From 5a932e8c77207188c73629da8ab80f4c401c4e76 Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 18 Jan 2013 15:21:02 +0000 Subject: Unset Asymmetric Patterns git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/QMicromega.v | 4 ++-- plugins/micromega/RingMicromega.v | 2 +- plugins/micromega/Tauto.v | 18 +++++++++--------- plugins/micromega/ZMicromega.v | 2 +- plugins/nsatz/Nsatz.v | 2 +- plugins/setoid_ring/Field_theory.v | 2 +- plugins/setoid_ring/Ncring_polynom.v | 4 ++-- 7 files changed, 17 insertions(+), 17 deletions(-) (limited to 'plugins') 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) -- cgit v1.2.3