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/Core | |
| 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/Core')
| -rw-r--r-- | flocq/Core/Fcore_defs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/flocq/Core/Fcore_defs.v b/flocq/Core/Fcore_defs.v index ad8cf4f5..01b868ab 100644 --- a/flocq/Core/Fcore_defs.v +++ b/flocq/Core/Fcore_defs.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} f. +Arguments Fexp {beta} f. 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} f. +Arguments Fexp {beta} f. +Arguments F2R {beta} f. Section RND. |