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 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/micromega/QMicromega.v') 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) -- cgit v1.2.3