From 2a6876b762f21e624a9138927dff5baf29086397 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 8 Jul 2018 18:03:44 +0200 Subject: Get rid of horrendous hack limiting the size of parsed integers --- parsing/g_prim.mlg | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 774db97f2..dfb788907 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -24,13 +24,9 @@ let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string loc s = try - let n = int_of_string s in - (* To avoid Array.make errors (that e.g. Undo uses), we set a *) - (* more restricted limit than int_of_string does *) - if n > 1024 * 2048 then raise Exit; - n - with Failure _ | Exit -> - CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") + int_of_string s + with Failure _ -> + CErrors.user_err ~loc (Pp.str "This number is too large.") } -- cgit v1.2.3