diff options
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 8bbb404..94a9917 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -442,8 +442,7 @@ Lemma decode_float32_cast: forall l, Float.singleoffloat (decode_float Mfloat32 l) = decode_float Mfloat32 l. Proof. - intros; unfold decode_float. rewrite <- Float.single_of_bits_of_single. - rewrite Float.bits_of_single_of_bits. auto. + intros; unfold decode_float. rewrite Float.singleoffloat_of_bits. auto. Qed. (** * Encoding and decoding values *) |