diff options
Diffstat (limited to 'flocq/Appli/Fappli_IEEE.v')
| -rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 2 |
1 files changed, 1 insertions, 1 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. |