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.

4 files changed, 14 insertions, 14 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.
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.
 
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
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.