diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-08 19:55:23 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-08 19:55:23 +0000 |
commit | d63320ceb1c56710f5e953742dd5d6cf43aacbdf (patch) | |
tree | 9a6eec0f6e330270aab09af8ae9c744282dc8a82 /plugins/syntax | |
parent | c9467e5684f9a71cb82ddc72b5b9d501b32b5c5e (diff) |
Uniformizing the [if_warn] flag used for warning printing and put
it into the standard logger instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
-rw-r--r-- | plugins/syntax/nat_syntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 8f34ec495..24ce7d652 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -25,7 +25,7 @@ let threshold = of_int 5000 let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than threshold n then - Flags.if_warn msg_warning + msg_warning (strbrk "Stack overflow or segmentation fault happens when " ++ strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ |