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_FLT.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq/Core/Fcore_FLT.v') 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. -- cgit