diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-12 10:10:50 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-12 10:10:50 +0100 |
| commit | e6308c5ec63a3a01ee33c9304e5249c6159dd1ef (patch) | |
| tree | a502121771580a3840f58240e8cb6178b3269d82 /lib/Integers.v | |
| parent | b125afc697c1214cb329967b506a4a740a942e81 (diff) | |
| download | compcert-kvx-e6308c5ec63a3a01ee33c9304e5249c6159dd1ef.tar.gz compcert-kvx-e6308c5ec63a3a01ee33c9304e5249c6159dd1ef.zip | |
Removed deprecated lemma.
The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 2 |
1 files changed, 1 insertions, 1 deletions
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: |