diff options
Diffstat (limited to 'parsing/g_prim.mlg')
-rw-r--r-- | parsing/g_prim.mlg | 10 |
1 files 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.") } |