From ddd8effe9fbee719e3a2d07f8338995d963ff630 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 10 Jul 2008 08:02:31 +0000 Subject: Bug résiduel du backtrack de coqide se produisant lorsque la limite de la pile de undo de tactique est atteinte (il ne fallait pas oublier de faire un abort). On en profite pour porter cette limite à une valeur significativement plus élevée. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11219 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_prim.ml4 | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'parsing') diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 8501b3436..deedf957d 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -23,6 +23,16 @@ open Nametab let local_make_qualid l id = make_qualid (make_dirpath 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 -> + Util.user_err_loc (loc,"",Pp.str "cannot support a so large number.") + GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident @@ -90,11 +100,11 @@ GEXTEND Gram [ [ s = STRING -> s ] ] ; integer: - [ [ i = INT -> int_of_string i - | "-"; i = INT -> - int_of_string i ] ] + [ [ i = INT -> my_int_of_string loc i + | "-"; i = INT -> - my_int_of_string loc i ] ] ; natural: - [ [ i = INT -> int_of_string i ] ] + [ [ i = INT -> my_int_of_string loc i ] ] ; bigint: (* Negative numbers are dealt with specially *) [ [ i = INT -> (Bigint.of_string i) ] ] -- cgit v1.2.3