diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
| commit | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (patch) | |
| tree | f54d8315891bec2f741545991f420dd4407bccc0 /flocq/Prop/Fprop_plus_error.v | |
| parent | 44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (diff) | |
| download | compcert-kvx-177c8fbc523a171e8c8470fa675f9a69ef7f99de.tar.gz compcert-kvx-177c8fbc523a171e8c8470fa675f9a69ef7f99de.zip | |
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/Prop/Fprop_plus_error.v')
| -rw-r--r-- | flocq/Prop/Fprop_plus_error.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v index 950ca267..41c2f031 100644 --- a/flocq/Prop/Fprop_plus_error.v +++ b/flocq/Prop/Fprop_plus_error.v @@ -157,7 +157,7 @@ Lemma round_plus_eq_zero_aux : (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z -> format x -> format y -> (0 <= x + y)%R -> - round beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = 0%R -> (x + y = 0)%R. Proof with auto with typeclass_instances. intros x y He Hx Hy Hp Hxy. @@ -202,11 +202,11 @@ Context { valid_rnd : Valid_rnd rnd }. Theorem round_plus_eq_zero : forall x y, format x -> format y -> - round beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = 0%R -> (x + y = 0)%R. Proof with auto with typeclass_instances. intros x y Hx Hy. -destruct (Rle_or_lt R0 (x + y)) as [H1|H1]. +destruct (Rle_or_lt 0 (x + y)) as [H1|H1]. (* . *) revert H1. destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2]. |