diff options
Diffstat (limited to 'flocq/Appli')
| -rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 2 | ||||
| -rw-r--r-- | flocq/Appli/Fappli_IEEE_bits.v | 14 |
2 files changed, 8 insertions, 8 deletions
diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index b6ccd84f..161b545a 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -46,7 +46,7 @@ End AnyRadix. Section Binary. -Implicit Arguments exist [[A] [P]]. +Arguments exist {A P} x _. (** [prec] is the number of bits of the mantissa including the implicit one; [emax] is the exponent of the infinities. diff --git a/flocq/Appli/Fappli_IEEE_bits.v b/flocq/Appli/Fappli_IEEE_bits.v index 87aa1046..e6a012cf 100644 --- a/flocq/Appli/Fappli_IEEE_bits.v +++ b/flocq/Appli/Fappli_IEEE_bits.v @@ -25,11 +25,11 @@ Require Import Fappli_IEEE. 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} x _. +Arguments B754_zero {prec emax} _. +Arguments B754_infinity {prec emax} _. +Arguments B754_nan {prec emax} _ _. +Arguments B754_finite {prec emax} _ m e _. (** Number of bits for the fraction and exponent *) Variable mw ew : Z. @@ -604,7 +604,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. @@ -647,7 +647,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. |