diff options
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 2 | ||||
-rw-r--r-- | flocq/Appli/Fappli_IEEE_bits.v | 14 | ||||
-rw-r--r-- | flocq/Calc/Fcalc_ops.v | 2 | ||||
-rw-r--r-- | flocq/Core/Fcore_defs.v | 10 |
5 files changed, 14 insertions, 17 deletions
@@ -147,9 +147,6 @@ endif proof: $(FILES:.v=.vo) -# Turn off some warnings for compiling Flocq -flocq/%.vo: COQCOPTS+=-w -deprecated-implicit-arguments - extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v 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. |