diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index c15e767f34710a55de28586de915e533ff0d4deb..a881b71694746b3f6618aa9965359110d8a2ec4a 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -420,20 +420,6 @@ module Make (F: Float_sig.S) = struct
     | FRange.NaN -> Comp.False
     | FRange.Itv (_b, _e, nan) -> if nan then Comp.Unknown else Comp.True
 
-  let is_pos_infinity = function
-    | FRange.NaN -> Comp.False
-    | FRange.Itv (b, e, _) ->
-      if not (Cmp.is_pos_infinity e) then Comp.False
-      else if not (Cmp.is_pos_infinity b) then Comp.Unknown
-      else Comp.True
-
-  let is_neg_infinity = function
-    | FRange.NaN -> Comp.False
-    | FRange.Itv (b, e, _) ->
-      if not (Cmp.is_neg_infinity b) then Comp.False
-      else if not (Cmp.is_neg_infinity e) then Comp.Unknown
-      else Comp.True
-
   let is_finite = function
     | FRange.NaN -> Comp.False
     | FRange.Itv (b, e, nan) ->
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index a5e2c88738f253f267a059f3737d96773c7f4393..53b9ae7ec2ed45f0d647612c340d210cb3648ba7 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -91,8 +91,6 @@ module type S = sig
 
   val is_finite: t -> Abstract_interp.Comp.result
   val is_not_nan: t -> Abstract_interp.Comp.result
-  val is_pos_infinity: t -> Abstract_interp.Comp.result
-  val is_neg_infinity: t -> Abstract_interp.Comp.result
   val backward_is_finite: positive:bool -> prec -> t -> t or_bottom
   val backward_is_nan: positive:bool -> t -> t or_bottom
 
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index e518c3b7b21634d46884d8530fc608796ff34a73..c40ad9050fdf45fbffcef7bdc8e7bfd4ad12dc54 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -2286,6 +2286,12 @@ and eval_predicate env pred =
     in
     match li.l_var_info.lv_name, args with
     | "\\is_finite", [arg] -> unary_float Fval.is_finite arg
+    | "\\is_plus_infinity", [arg] ->
+      let pos_inf = Fval.pos_infinity Float_sig.Single in
+      unary_float (fun f -> Fval.forward_comp Comp.Eq f pos_inf) arg
+    | "\\is_minus_infinity", [arg] ->
+      let neg_inf = Fval.neg_infinity Float_sig.Single in
+      unary_float (fun f -> Fval.forward_comp Comp.Eq f neg_inf) arg
     | "\\is_NaN", [arg] -> inv_truth (unary_float Fval.is_not_nan arg)
     | ("\\eq_float" | "\\eq_double"), [arg1;arg2] -> fval_cmp Comp.Eq arg1 arg2
     | ("\\ne_float" | "\\ne_double"), [arg1;arg2] -> fval_cmp Comp.Ne arg1 arg2
@@ -2301,8 +2307,6 @@ and eval_predicate env pred =
           Value_parameters.abort
             "Wrong argument: \\warning expects a constant string"
       end
-    | "\\is_plus_infinity", [arg] -> unary_float Fval.is_pos_infinity arg
-    | "\\is_minus_infinity", [arg] -> unary_float Fval.is_neg_infinity arg
     | "\\subset", [argl;argr] -> begin
         try
           let l = eval_term ~alarm_mode env argl in