From 78e75ff116752a497343fc0cbb91c060a7d79a0a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 9 Nov 2017 11:28:37 +0100 Subject: [PATCH] Avoid warning due to 'Implicit Arguments'. --- src/Calc/Operations.v | 2 +- src/Core/Definitions.v | 10 +++++----- src/IEEE754/Binary.v | 2 +- src/IEEE754/Bits.v | 17 ++++++++++------- 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/Calc/Operations.v b/src/Calc/Operations.v index 7d75ec3..dae9163 100644 --- a/src/Calc/Operations.v +++ b/src/Calc/Operations.v @@ -26,7 +26,7 @@ Variable beta : radix. Notation bpow e := (bpow beta e). -Implicit Arguments Float [[beta]]. +Arguments Float {beta}. Definition Falign (f1 f2 : float beta) := let '(Float m1 e1) := f1 in diff --git a/src/Core/Definitions.v b/src/Core/Definitions.v index 8eb11e3..686d288 100644 --- a/src/Core/Definitions.v +++ b/src/Core/Definitions.v @@ -25,8 +25,8 @@ Section Def. (** Definition of a floating-point number *) Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }. -Implicit Arguments Fnum [[beta]]. -Implicit Arguments Fexp [[beta]]. +Arguments Fnum {beta}. +Arguments Fexp {beta}. Variable beta : radix. @@ -46,9 +46,9 @@ Definition round_pred (P : R -> R -> Prop) := End Def. -Implicit Arguments Fnum [[beta]]. -Implicit Arguments Fexp [[beta]]. -Implicit Arguments F2R [[beta]]. +Arguments Fnum {beta}. +Arguments Fexp {beta}. +Arguments F2R {beta}. Section RND. diff --git a/src/IEEE754/Binary.v b/src/IEEE754/Binary.v index 4a811e8..71a5e72 100644 --- a/src/IEEE754/Binary.v +++ b/src/IEEE754/Binary.v @@ -38,7 +38,7 @@ End AnyRadix. Section Binary. -Implicit Arguments exist [[A] [P]]. +Arguments exist {A} {P}. (** [prec] is the number of bits of the mantissa including the implicit one; [emax] is the exponent of the infinities. diff --git a/src/IEEE754/Bits.v b/src/IEEE754/Bits.v index 3b6b927..c7622be 100644 --- a/src/IEEE754/Bits.v +++ b/src/IEEE754/Bits.v @@ -22,11 +22,11 @@ Require Import Core Digits Binary. Section Binary_Bits. -Implicit Arguments exist [[A] [P]]. -Implicit Arguments B754_zero [[prec] [emax]]. -Implicit Arguments B754_infinity [[prec] [emax]]. -Implicit Arguments B754_nan [[prec] [emax]]. -Implicit Arguments B754_finite [[prec] [emax]]. +Arguments exist {A} {P}. +Arguments B754_zero {prec} {emax}. +Arguments B754_infinity {prec} {emax}. +Arguments B754_nan {prec} {emax}. +Arguments B754_finite {prec} {emax}. (** Number of bits for the fraction and exponent *) Variable mw ew : Z. @@ -39,17 +39,20 @@ Let emin := (3 - emax - prec)%Z. Let binary_float := binary_float prec emax. Let Hprec : (0 < prec)%Z. +Proof. unfold prec. apply Zle_lt_succ. now apply Zlt_le_weak. Qed. Let Hm_gt_0 : (0 < 2^mw)%Z. +Proof. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. Qed. Let He_gt_0 : (0 < 2^ew)%Z. +Proof. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. Qed. @@ -602,7 +605,7 @@ End Binary_Bits. (** Specialization for IEEE single precision operations *) Section B32_Bits. -Implicit Arguments B754_nan [[prec] [emax]]. +Arguments B754_nan {prec} {emax}. Definition binary32 := binary_float 24 128. @@ -645,7 +648,7 @@ End B32_Bits. (** Specialization for IEEE double precision operations *) Section B64_Bits. -Implicit Arguments B754_nan [[prec] [emax]]. +Arguments B754_nan {prec} {emax}. Definition binary64 := binary_float 53 1024. -- GitLab