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.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.v')
| -rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 2 |
1 files changed, 1 insertions, 1 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. |