diff options
| author | Maxime Dénès | 2018-06-11 10:02:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-17 09:33:30 +0200 |
| commit | 7a4b3edf1a4299c7813668515ad1b8fa6cf99dd3 (patch) | |
| tree | 214e4e58db8d7132168cc5ba47dae1b022fbd684 /kernel | |
| parent | 00a63b73f267ae90cc868f14ab4f36db8185b3e0 (diff) | |
[VM] Allocate a bit less in digits_from_uint
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/clambda.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index cc50e375f4..0a3fb44cbe 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -836,10 +836,11 @@ let dynamic_int31_compilation fc args = if not fc then raise Not_found else Luint (UintDigits args) +let d0 = Lint 0 +let d1 = Lint 1 + (* We are relying here on the tags of digits constructors *) let digits_from_uint i = - let d0 = Lint 0 in - let d1 = Lint 1 in let digits = Array.make 31 d0 in for k = 0 to 30 do if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then |