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.