Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 4bb89f65 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Reduced dependencies of Fprop_plup_error. Marked lemmas as such and fixed comment.

parent 24cf49f7
......@@ -17,8 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Error of the multiplication is in generic format and rounding to nearest *)
Require Import Fcore.
(** * Error of the rounded-to-nearest addition is representable. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Section Fprop_plus_error.
......@@ -65,7 +69,7 @@ Notation format := (generic_format beta fexp).
Variable choice : R -> bool.
Theorem plus_error_aux :
Lemma plus_error_aux :
forall x y,
(canonic_exponent beta fexp x <= canonic_exponent beta fexp y)%Z ->
format x -> format y ->
......@@ -138,7 +142,7 @@ Notation format := (generic_format beta fexp).
Hypothesis not_FTZ : not_FTZ_prop fexp.
Theorem round_plus_eq_zero_aux :
Lemma round_plus_eq_zero_aux :
forall rnd x y,
(canonic_exponent beta fexp x <= canonic_exponent beta fexp y)%Z ->
format x -> format y ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment