diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/DecimalQ.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/HexadecimalQ.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v index d2cd061594..f666c29643 100644 --- a/theories/Numbers/DecimalQ.v +++ b/theories/Numbers/DecimalQ.v @@ -15,7 +15,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q. +Lemma of_to (q:IQ) : forall d, to_decimal q = Some d -> of_decimal d = q. Admitted. (* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *) diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v index ce6f074d70..b773aede8c 100644 --- a/theories/Numbers/HexadecimalQ.v +++ b/theories/Numbers/HexadecimalQ.v @@ -16,7 +16,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ. Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. +Lemma of_to (q:IQ) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. Admitted. (* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *) |