From 1c77deb420e626aa79d5b7db15231c887cd7d870 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 23:29:25 +0100
Subject: minor implicit issue

---
 lib/IEEE754_extra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index ed3d9f1f..a76daab4 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1167,7 +1167,7 @@ Proof.
     unfold Z.succ. rewrite plus_IZR. lra.
 Qed.
 
-Lemma Rabs_le_rev : forall {a} {b}, (Rabs a <= b -> -b <= a <= b)%R.
+Lemma Rabs_le_rev : forall a b, (Rabs a <= b -> -b <= a <= b)%R.
 Proof.
   intros a b ABS.
   unfold Rabs in ABS.
@@ -1179,7 +1179,7 @@ Theorem ZofB_ne_range:
 Proof.
   intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H.
   pose proof (Znearest_imp2  (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS.
-  pose proof (Rabs_le_rev ABS).
+  pose proof (Rabs_le_rev _ _ ABS).
   lra.
 Qed.
 
-- 
cgit