summaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN/Nbasic.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
commit6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch)
treeb04b45d1a6f42d19b1428c522d647afbad2f9b83 /theories/Numbers/Natural/BigN/Nbasic.v
parent3e96002677226c0cdaa8f355938a76cfb37a722a (diff)
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'theories/Numbers/Natural/BigN/Nbasic.v')
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v11
1 files changed, 2 insertions, 9 deletions
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