From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/QArith/Qround.v | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

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

diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 0ed6d557..7c5ddbb6 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import QArith.
@@ -78,11 +80,11 @@ unfold Qlt.
 simpl.
 replace (n*1)%Z with n by ring.
 ring_simplify.
-replace (n / ' d * ' d + ' d)%Z with
-  (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
+replace (n / Zpos d * Zpos d + Zpos d)%Z with
+  ((Zpos d * (n / Zpos d) + n mod Zpos  d) + Zpos  d - n mod Zpos d)%Z by ring.
 rewrite <- Z_div_mod_eq; auto with*.
 rewrite <- Z.lt_add_lt_sub_r.
-destruct (Z_mod_lt n ('d)); auto with *.
+destruct (Z_mod_lt n (Zpos d)); auto with *.
 Qed.
 
 Hint Resolve Qlt_floor : qarith.
@@ -105,9 +107,9 @@ Proof.
 intros [xn xd] [yn yd] Hxy.
 unfold Qle in *.
 simpl in *.
-rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
-rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
-rewrite (Z.mul_comm ('yd) ('xd)).
+rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.
+rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.
+rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
 apply Z_div_le; auto with *.
 Qed.
 
@@ -141,7 +143,7 @@ Qed.
 Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
 Proof.
  unfold Qfloor. intros. simpl.
- destruct m as [?|?|p]; simpl.
+ destruct m as [ | | p]; simpl.
   now rewrite Zdiv_0_r, Z.mul_0_r.
   now rewrite Z.mul_1_r.
  rewrite <- Z.opp_eq_mul_m1.
-- 
cgit v1.2.3