From fcebe5a64bb253862e52503b7d4dd6c4c1aebcdf Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Oct 2019 13:55:35 +0000
Subject: QArith: only depend on ZArith_base

---
 theories/QArith/QArith_base.v | 2 +-
 theories/QArith/Qround.v      | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 54d35cded2..4239943d03 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Export ZArith.
+Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Morphisms Setoid Bool.
 
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 8d68038582..35f113e226 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import QArith.
+Import Zdiv.
 
 Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
 Proof.
@@ -38,7 +39,7 @@ Proof.
 intros z.
 unfold Qceiling.
 simpl.
-rewrite Zdiv_1_r.
+rewrite Z.div_1_r.
 apply Z.opp_involutive.
 Qed.
 
@@ -50,8 +51,7 @@ unfold Qle.
 simpl.
 replace (n*1)%Z with n by ring.
 rewrite Z.mul_comm.
-apply Z_mult_div_ge.
-auto with *.
+now apply Z.mul_div_le.
 Qed.
 
 Hint Resolve Qfloor_le : qarith.
-- 
cgit v1.2.3