diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
| commit | 234f5479773d43a48e67c5c0ea361445c7fb6782 (patch) | |
| tree | 0609f0aef4769561d3bee2049c5c973f40b20be3 /kernel | |
| parent | 32415df7e24d4d79a00fae95a5f619980b006c61 (diff) | |
Correct some spelling errorsmaster
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
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 f1b6f3dff..32a4bd650 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -763,7 +763,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 *) |