From dce9ff8da2710aa81fbcf6d1498de35ea9ad06f4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 13 Feb 2017 10:28:35 +0100 Subject: Update Flocq to version 2.5.2 This version of Flocq is compatible with Coq 8.6 --- flocq/Core/Fcore_Raux.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq/Core/Fcore_Raux.v') diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index d728e0ba..939002cf 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -1673,7 +1673,7 @@ Qed. (** Another well-used function for having the logarithm of a real number x to the base #β# *) Record ln_beta_prop x := { ln_beta_val :> Z ; - _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R + _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R }. Definition ln_beta : -- cgit