diff options
| author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-28 07:15:20 -0700 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-03-28 16:15:20 +0200 |
| commit | 5e665ecc84eac83bd0a545995d161d83fbed9e25 (patch) | |
| tree | 75748780b3e6b288c0386b19cb5d71083d1bb7a5 /flocq/Appli/Fappli_IEEE_bits.v | |
| parent | fbc778079d50a4af45b9a648eab56cef29ac75f4 (diff) | |
| download | compcert-kvx-5e665ecc84eac83bd0a545995d161d83fbed9e25.tar.gz compcert-kvx-5e665ecc84eac83bd0a545995d161d83fbed9e25.zip | |
Change Implicit Arguments to Arguments (#225)
Implicit Arguments is deprecated in Coq since 8.6 or so.
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
Diffstat (limited to 'flocq/Appli/Fappli_IEEE_bits.v')
| -rw-r--r-- | flocq/Appli/Fappli_IEEE_bits.v | 14 |
1 files changed, 7 insertions, 7 deletions
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. |