diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
commit | 2dd133f9178ae285d3939f29479b4acd9dad394d (patch) | |
tree | a89023c15848438f84b47663633f34960b9bcfbc /flocq/Core/Raux.v | |
parent | c34d25e011402aedad62b3fe9b7b04989df4522e (diff) | |
download | compcert-2dd133f9178ae285d3939f29479b4acd9dad394d.tar.gz compcert-2dd133f9178ae285d3939f29479b4acd9dad394d.zip |
Update the vendored Flocq library to version 3.4.2
For compatibility with the upcoming Coq 8.14.
Diffstat (limited to 'flocq/Core/Raux.v')
-rw-r--r-- | flocq/Core/Raux.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 455190dc..221d84d6 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -18,7 +18,7 @@ COPYING file for more details. *) (** * Missing definitions/lemmas *) -Require Export Psatz. +Require Import Psatz. Require Export Reals ZArith. Require Export Zaux. @@ -1277,7 +1277,7 @@ Theorem Zfloor_div : Zfloor (IZR x / IZR y) = (x / y)%Z. Proof. intros x y Zy. -generalize (Z_div_mod_eq_full x y Zy). +generalize (Z.div_mod x y Zy). intros Hx. rewrite Hx at 1. assert (Zy': IZR y <> 0%R). |