diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-03-08 14:07:33 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-03-08 14:07:33 +0100 |
| commit | a968152051941a0fc50a86c3fc15e90e22ed7c47 (patch) | |
| tree | 70f2590a8ea026c2f8596220e60b829d21b6398c /flocq/Core/Fcore_FLT.v | |
| parent | de24549f572deb6519be2216ef364b7c80bfdece (diff) | |
| parent | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (diff) | |
| download | compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.tar.gz compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.zip | |
Merge pull request #175 from silene/IZR
Adapt proofs to future handling of literal constants in Coq
This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
Diffstat (limited to 'flocq/Core/Fcore_FLT.v')
| -rw-r--r-- | flocq/Core/Fcore_FLT.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index 372af6ad..53dc48a7 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -187,7 +187,7 @@ Qed. (** Links between FLT and FIX (underflow) *) Theorem canonic_exp_FLT_FIX : - forall x, x <> R0 -> + forall x, x <> 0%R -> (Rabs x < bpow (emin + prec))%R -> canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x. Proof. |