diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/syntax/nat_syntax.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c62c81377..5d20c2a3c 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -33,7 +33,7 @@ open Names let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than (of_string "5000") n then - Flags.if_warn msg_warning + Flags.if_warn 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 " ++ @@ -41,11 +41,11 @@ let nat_of_int dloc n = let ref_O = RRef (dloc, glob_O) in let ref_S = RRef (dloc, glob_S) in let rec mk_nat acc n = - if n <> zero then + if n <> zero then mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n) - else + else acc - in + in mk_nat ref_O n end else @@ -61,9 +61,9 @@ let rec int_of_nat = function | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) | RRef (_,z) when z = glob_O -> zero | _ -> raise Non_closed_number - + let uninterp_nat p = - try + try Some (int_of_nat p) with Non_closed_number -> None |