From 177c8fbc523a171e8c8470fa675f9a69ef7f99de Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 8 Mar 2017 08:35:29 +0100 Subject: 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. --- flocq/Core/Fcore_float_prop.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'flocq/Core/Fcore_float_prop.v') diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v index 8199ede6..a183bf0a 100644 --- a/flocq/Core/Fcore_float_prop.v +++ b/flocq/Core/Fcore_float_prop.v @@ -136,7 +136,7 @@ Qed. (** Sign facts *) Theorem F2R_0 : forall e : Z, - F2R (Float beta 0 e) = R0. + F2R (Float beta 0 e) = 0%R. Proof. intros e. unfold F2R. simpl. @@ -145,7 +145,7 @@ Qed. Theorem F2R_eq_0_reg : forall m e : Z, - F2R (Float beta m e) = R0 -> + F2R (Float beta m e) = 0%R -> m = Z0. Proof. intros m e H. -- cgit