From 9b3bb6e23d7235a39eb6bfca9c4fa2eca807953f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 26 Jan 2024 17:21:57 +0100 Subject: [PATCH] [lib] use stdlib function --- src/libraries/utils/floating_point.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml index f3349ba07a7..aa389e9f96d 100644 --- a/src/libraries/utils/floating_point.ml +++ b/src/libraries/utils/floating_point.ml @@ -113,10 +113,6 @@ let num_dot_frac = Str.regexp (reg_numopt ^ reg_dot ^ reg_numopt) let num_dot_frac_exp = Str.regexp (reg_numopt ^ reg_dot ^ reg_numopt ^ reg_exp) let num_exp = Str.regexp (reg_num ^ reg_exp) -let float_of_string_opt s = - try Some (float_of_string s) - with Failure _ -> None - let sys_single_precision_of_string_opt s = try Some (sys_single_precision_of_string s) with Failure _ -> None -- GitLab