From e6308c5ec63a3a01ee33c9304e5249c6159dd1ef Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 12 Mar 2018 10:10:50 +0100
Subject: Removed deprecated lemma.

The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199
---
 lib/Integers.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/Integers.v')

diff --git a/lib/Integers.v b/lib/Integers.v
index 7fb29803..a905a7d1 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1181,7 +1181,7 @@ Qed.
 Theorem divs_one:
   forall x, zwordsize > 1 -> divs x one = x.
 Proof.
-  unfold divs; intros. rewrite signed_one. rewrite Zquot_1_r. apply repr_signed. auto.
+  unfold divs; intros. rewrite signed_one. rewrite Z.quot_1_r. apply repr_signed. auto.
 Qed.
 
 Theorem modu_one:
-- 
cgit