diff options
| author | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
| commit | fca9ec68937e047d3895d05e57de462387737796 (patch) | |
| tree | f6fc75f7e6be6b60ceafff3afa9d7e13b3219571 /kernel | |
| parent | b7dae2c97cce2a298bfbbd6f3a72a02e092ebe9e (diff) | |
| parent | 06cd051d140a183229cd43f0bbae152d6ad8d6ca (diff) | |
Merge PR #8589: Correct some spelling errors (continued)
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/clambda.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index c21ce22421..1e4dbfd418 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -764,7 +764,7 @@ and lambda_of_app env f args = and such, which can't be done at this time. for instance, for int31: if one of the digit is not closed, it's not impossible that the number - gets fully instanciated at run-time, thus to ensure + gets fully instantiated at run-time, thus to ensure uniqueness of the representation in the vm it is necessary to try and build a caml integer during the execution *) |