Commit e46760a7 authored by Jasper Hugunin's avatar Jasper Hugunin Committed by Guillaume Melquiond

Change Implicit Arguments to Arguments

parent 2ac98b06
...@@ -46,7 +46,7 @@ End AnyRadix. ...@@ -46,7 +46,7 @@ End AnyRadix.
Section Binary. 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; (** [prec] is the number of bits of the mantissa including the implicit one;
[emax] is the exponent of the infinities. [emax] is the exponent of the infinities.
......
...@@ -25,11 +25,11 @@ Require Import Fappli_IEEE. ...@@ -25,11 +25,11 @@ Require Import Fappli_IEEE.
Section Binary_Bits. Section Binary_Bits.
Implicit Arguments exist [[A] [P]]. Arguments exist {A P} x _.
Implicit Arguments B754_zero [[prec] [emax]]. Arguments B754_zero {prec emax} _.
Implicit Arguments B754_infinity [[prec] [emax]]. Arguments B754_infinity {prec emax} _.
Implicit Arguments B754_nan [[prec] [emax]]. Arguments B754_nan {prec emax} _ _.
Implicit Arguments B754_finite [[prec] [emax]]. Arguments B754_finite {prec emax} _ m e _.
(** Number of bits for the fraction and exponent *) (** Number of bits for the fraction and exponent *)
Variable mw ew : Z. Variable mw ew : Z.
...@@ -604,7 +604,7 @@ End Binary_Bits. ...@@ -604,7 +604,7 @@ End Binary_Bits.
(** Specialization for IEEE single precision operations *) (** Specialization for IEEE single precision operations *)
Section B32_Bits. Section B32_Bits.
Implicit Arguments B754_nan [[prec] [emax]]. Arguments B754_nan {prec emax} _ _.
Definition binary32 := binary_float 24 128. Definition binary32 := binary_float 24 128.
...@@ -647,7 +647,7 @@ End B32_Bits. ...@@ -647,7 +647,7 @@ End B32_Bits.
(** Specialization for IEEE double precision operations *) (** Specialization for IEEE double precision operations *)
Section B64_Bits. Section B64_Bits.
Implicit Arguments B754_nan [[prec] [emax]]. Arguments B754_nan {prec emax} _ _.
Definition binary64 := binary_float 53 1024. Definition binary64 := binary_float 53 1024.
......
...@@ -28,7 +28,7 @@ Variable beta : radix. ...@@ -28,7 +28,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e). Notation bpow e := (bpow beta e).
Implicit Arguments Float [[beta]]. Arguments Float {beta} Fnum Fexp.
Definition Falign (f1 f2 : float beta) := Definition Falign (f1 f2 : float beta) :=
let '(Float m1 e1) := f1 in let '(Float m1 e1) := f1 in
......
...@@ -25,8 +25,8 @@ Section Def. ...@@ -25,8 +25,8 @@ Section Def.
(** Definition of a floating-point number *) (** Definition of a floating-point number *)
Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }. Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }.
Implicit Arguments Fnum [[beta]]. Arguments Fnum {beta} f.
Implicit Arguments Fexp [[beta]]. Arguments Fexp {beta} f.
Variable beta : radix. Variable beta : radix.
...@@ -46,9 +46,9 @@ Definition round_pred (P : R -> R -> Prop) := ...@@ -46,9 +46,9 @@ Definition round_pred (P : R -> R -> Prop) :=
End Def. End Def.
Implicit Arguments Fnum [[beta]]. Arguments Fnum {beta} f.
Implicit Arguments Fexp [[beta]]. Arguments Fexp {beta} f.
Implicit Arguments F2R [[beta]]. Arguments F2R {beta} f.
Section RND. Section RND.
......
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