From f2ea9fec68e0ae8193381513f650321c1b1f6900 Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 2 Jul 2007 14:29:16 +0000
Subject: Correction (partielle) du bug #1587

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9931 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/QArith/QArith_base.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 198fedd551..6e18490108 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -38,8 +38,8 @@ Notation " 1 " := (1#1) : Q_scope.
 Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
 Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
 Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z.
-Notation Qgt := (fun x y : Q => Qlt y x).
-Notation Qge := (fun x y : Q => Qle y x).
+Notation Qgt := (fun a b : Q => Qlt b a).
+Notation Qge := (fun a b : Q => Qle b a).
 
 Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
 Infix "<" := Qlt : Q_scope.
-- 
cgit v1.2.3