Commit 78e75ff1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid warning due to 'Implicit Arguments'.

parent fc6c63d2
......@@ -26,7 +26,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Implicit Arguments Float [[beta]].
Arguments Float {beta}.
Definition Falign (f1 f2 : float beta) :=
let '(Float m1 e1) := f1 in
......
......@@ -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}.
Arguments Fexp {beta}.
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}.
Arguments Fexp {beta}.
Arguments F2R {beta}.
Section RND.
......
......@@ -38,7 +38,7 @@ End AnyRadix.
Section Binary.
Implicit Arguments exist [[A] [P]].
Arguments exist {A} {P}.
(** [prec] is the number of bits of the mantissa including the implicit one;
[emax] is the exponent of the infinities.
......
......@@ -22,11 +22,11 @@ Require Import Core Digits Binary.
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}.
Arguments B754_zero {prec} {emax}.
Arguments B754_infinity {prec} {emax}.
Arguments B754_nan {prec} {emax}.
Arguments B754_finite {prec} {emax}.
(** Number of bits for the fraction and exponent *)
Variable mw ew : Z.
......@@ -39,17 +39,20 @@ Let emin := (3 - emax - prec)%Z.
Let binary_float := binary_float prec emax.
Let Hprec : (0 < prec)%Z.
Proof.
unfold prec.
apply Zle_lt_succ.
now apply Zlt_le_weak.
Qed.
Let Hm_gt_0 : (0 < 2^mw)%Z.
Proof.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
Let He_gt_0 : (0 < 2^ew)%Z.
Proof.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
......@@ -602,7 +605,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.
......@@ -645,7 +648,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.
......
  • Jasper Hugunin
    @jasperh started a thread
    Last updated by DENES Maxime
    • I am working on removing the Implicit Arguments command completely (https://github.com/coq/coq/pull/6802). When can the renaming branch be expected to be merged? If it is not expected to be merged for some time, would you consider cherry-picking this commit onto master?

    • would you consider cherry-picking this commit onto master?

      The master branch supports Coq versions as old as 8.4. Unfortunately, these versions provide a fairly broken Arguments command, so this commit cannot be cherry-picked onto master.

    • @melquion When do you plan to drop 8.4 support? Maybe we could try to sync the removal of Implicit Arguments, if that's not too distant.

    • The renaming branch (aka Flocq 3.0) drops support for pre-8.7 versions. We intend to release it for early March. (Given that we were promising it for last November, that would not be too bad.)

    • Ok, so I guess it would make sense to merge the removal of Implicit Arguments only after 8.8. Especially given that warnings were not printed until 8.6.

    Please register or sign in to reply
  • mentioned in issue #1 (closed)

    Toggle commit list
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment