From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- theories/Numbers/Natural/BigN/Nbasic.v | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'theories/Numbers/Natural/BigN/Nbasic.v') diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index a531b92e..3741c95d 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -260,13 +260,6 @@ Section ReduceRec. End ReduceRec. -Definition opp_compare cmp := - match cmp with - | Lt => Gt - | Eq => Eq - | Gt => Lt - end. - Section CompareRec. Variable wm w : Type. @@ -447,7 +440,7 @@ End AddS. | Lt => y < x | Gt => y > x end -> - match opp_compare u with + match CompOpp u with | Eq => x = y | Lt => x < y | Gt => x > y -- cgit v1.2.3