diff --git a/src/Calc/Operations.v b/src/Calc/Operations.v index 7d75ec3a9c02f6834ddd9bfb04eddd2694feef54..dae9163ee14dc38d79f2aa8676523d5a75d20314 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 8eb11e391965ba4b87025e969c246e11be7e1404..686d288fa00853ad71ecf8ca358a3c929eb03c15 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 4a811e892d65c12f4f7110a84108bd62a01c89c9..71a5e72cea4326a3c07973144f35dcbc719b52d4 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 3b6b9275b3b00c8b2cc96dd2ca13e56d036f0d1b..c7622be88d2c0b3b2c873f80a4ee0ac982e35ba3 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.