From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/ZArith/Zcompare.v | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'theories/ZArith/Zcompare.v')

diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 20e1b006..fe91698f 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -1,13 +1,13 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Binary Integers : results about Zcompare *)
+(** Binary Integers : results about Z.compare *)
 (** Initial author: Pierre Crégut (CNET, Lannion, France *)
 
 (** THIS FILE IS DEPRECATED.
@@ -85,7 +85,7 @@ Qed.
 
 Lemma Zcompare_succ_compat n m : (Z.succ n ?= Z.succ m) = (n ?= m).
 Proof.
- rewrite <- 2 Z.add_1_l. apply Zcompare_plus_compat.
+ rewrite <- 2 Z.add_1_l. apply Z.add_compare_mono_l.
 Qed.
 
 (** * Multiplication and comparison *)
@@ -106,7 +106,7 @@ Qed.
 Lemma Zmult_compare_compat_r n m p :
   p > 0 -> (n ?= m) = (n * p ?= m * p).
 Proof.
- intros; rewrite 2 (Zmult_comm _ p); now apply Zmult_compare_compat_l.
+ intros; rewrite 2 (Z.mul_comm _ p); now apply Zmult_compare_compat_l.
 Qed.
 
 (** * Relating [x ?= y] to [=], [<=], [<], [>=] or [>] *)
@@ -181,18 +181,18 @@ Qed.
 
 (** Compatibility notations *)
 
-Notation Zcompare_refl := Z.compare_refl (only parsing).
-Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
-Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
-Notation Zcompare_spec := Z.compare_spec (only parsing).
-Notation Zmin_l := Z.min_l (only parsing).
-Notation Zmin_r := Z.min_r (only parsing).
-Notation Zmax_l := Z.max_l (only parsing).
-Notation Zmax_r := Z.max_r (only parsing).
-Notation Zabs_eq := Z.abs_eq (only parsing).
-Notation Zabs_non_eq := Z.abs_neq (only parsing).
-Notation Zsgn_0 := Z.sgn_null (only parsing).
-Notation Zsgn_1 := Z.sgn_pos (only parsing).
-Notation Zsgn_m1 := Z.sgn_neg (only parsing).
+Notation Zcompare_refl := Z.compare_refl (compat "8.3").
+Notation Zcompare_Eq_eq := Z.compare_eq (compat "8.3").
+Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (compat "8.3").
+Notation Zcompare_spec := Z.compare_spec (compat "8.3").
+Notation Zmin_l := Z.min_l (compat "8.3").
+Notation Zmin_r := Z.min_r (compat "8.3").
+Notation Zmax_l := Z.max_l (compat "8.3").
+Notation Zmax_r := Z.max_r (compat "8.3").
+Notation Zabs_eq := Z.abs_eq (compat "8.3").
+Notation Zabs_non_eq := Z.abs_neq (compat "8.3").
+Notation Zsgn_0 := Z.sgn_null (compat "8.3").
+Notation Zsgn_1 := Z.sgn_pos (compat "8.3").
+Notation Zsgn_m1 := Z.sgn_neg (compat "8.3").
 
 (** Not kept: Zcompare_egal_dec *)
-- 
cgit v1.2.3