From 42fdbab0d8c6266ba596f07d6fa482eb29736d44 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 2 Aug 2012 10:10:33 +0000
Subject: Bigint: new functions of_int and to_int, 2nd arg of pow in int

 * Many of_string and to_string could be replaced by of_int and to_int
   when the number isn't too large. NB: to_int may raise a Failure
   if the number is larger than max_int.

 * In numbers_syntax, computing the height of bigN trees via bigint
   is *really* overkill, int should be enough there : this limits
   printable/parsable bigN to (2^31)^(2^max_int) ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/syntax/nat_syntax.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax/nat_syntax.ml')

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 2fb8ce4511..34a6a1a749 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -30,9 +30,11 @@ open Names
 (* Parsing via scopes *)
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 
+let threshold = of_int 5000
+
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than (of_string "5000") n then
+      if less_than threshold n then
 	Flags.if_warn msg_warning
 	  (strbrk "Stack overflow or segmentation fault happens when " ++
 	   strbrk "working with large numbers in nat (observed threshold " ++
-- 
cgit v1.2.3