diff options
| author | letouzey | 2005-08-19 19:51:02 +0000 |
|---|---|---|
| committer | letouzey | 2005-08-19 19:51:02 +0000 |
| commit | be6ee173206a929ad664ff507334ad5add7ad157 (patch) | |
| tree | bfc3228af152a38598bc09798c5602d5e5953148 /lib | |
| parent | 66a2d880e14c1635f29cef0ad0113185cba29a18 (diff) | |
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bigint.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml index 40e04cc342..680424275a 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -75,10 +75,11 @@ let normalize_neg n = let k = ref 1 in while !k < Array.length n & n.(!k) = base - 1 do incr k done; let n' = Array.sub n !k (Array.length n - !k) in - if n' = [||] then [|-1|] else (n'.(0) <- n'.(0) - base; n') + if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') let rec normalize n = - if n=[||] then n else if n.(0) = -1 then normalize_neg n else normalize_pos n + if Array.length n = 0 then n else + if n.(0) = -1 then normalize_neg n else normalize_pos n let neg m = if m = zero then zero else @@ -254,7 +255,7 @@ let of_string s = a let to_string_pos sgn n = - if n = [||] then "0" else + if Array.length n = 0 then "0" else sgn ^ String.concat "" (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n))) |