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/Calc/Fcalc_ops.v | |
parent | fbc778079d50a4af45b9a648eab56cef29ac75f4 (diff) | |
download | compcert-5e665ecc84eac83bd0a545995d161d83fbed9e25.tar.gz compcert-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/Calc/Fcalc_ops.v')
-rw-r--r-- | flocq/Calc/Fcalc_ops.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Calc/Fcalc_ops.v b/flocq/Calc/Fcalc_ops.v index e3b059d1..e834c044 100644 --- a/flocq/Calc/Fcalc_ops.v +++ b/flocq/Calc/Fcalc_ops.v @@ -28,7 +28,7 @@ Variable beta : radix. Notation bpow e := (bpow beta e). -Implicit Arguments Float [[beta]]. +Arguments Float {beta} Fnum Fexp. Definition Falign (f1 f2 : float beta) := let '(Float m1 e1) := f1 in |