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/QArith/Qcanon.v | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'theories/QArith/Qcanon.v')

diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index fea2ba39..d1160cbe 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  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        *)
@@ -22,39 +22,39 @@ Arguments Qcmake this%Q _.
 Open Scope Qc_scope.
 
 Lemma Qred_identity :
-  forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
+  forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
 Proof.
   unfold Qred; intros (a,b); simpl.
-  generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)).
+  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)).
   intros.
   rewrite H1 in H; clear H1.
-  destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
   destruct H0.
-  rewrite Zmult_1_l in H, H0.
+  rewrite Z.mul_1_l in H, H0.
   subst; simpl; auto.
 Qed.
 
 Lemma Qred_identity2 :
-  forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
+  forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   unfold Qred; intros (a,b); simpl.
-  generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)).
+  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)).
   intros.
   rewrite <- H; rewrite <- H in H1; clear H.
-  destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
   injection H2; intros; clear H2.
   destruct H0.
   clear H0 H3.
   destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
   f_equal.
-  apply Pmult_reg_r with bb.
+  apply Pos.mul_reg_r with bb.
   injection H2; intros.
   rewrite <- H0.
   rewrite H; simpl; auto.
   elim H1; auto.
 Qed.
 
-Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z.
+Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   split; intros.
   apply Qred_identity2; auto.
@@ -488,7 +488,7 @@ Definition Qc_eq_bool (x y : Qc) :=
 
 Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y.
 Proof.
-  intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto.
+  intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto.
   intros _ H; inversion H.
 Qed.
 
-- 
cgit v1.2.3