From 5e665ecc84eac83bd0a545995d161d83fbed9e25 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 28 Mar 2018 07:15:20 -0700 Subject: 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. --- flocq/Calc/Fcalc_ops.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq/Calc') 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 -- cgit