diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-02 10:10:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-02 10:10:33 +0000 |
| commit | 42fdbab0d8c6266ba596f07d6fa482eb29736d44 (patch) | |
| tree | 548190ef9445adea5454fb324cb110b222aceec5 /plugins/syntax/nat_syntax.ml | |
| parent | fc6c6a6f4c0e9365a3040c3fae380f94af184fd0 (diff) | |
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
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 2fb8ce451..34a6a1a74 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 " ++ |