diff options
| author | Guillaume Melquiond | 2015-10-13 18:30:47 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-10-13 18:30:47 +0200 |
| commit | ed95f122f3c68becc09c653471dc2982b346d343 (patch) | |
| tree | 87e323b2d382c285e1eae864338ea397fda0923d /kernel/nativecode.ml | |
| parent | 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff) | |
Fix some typos.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 687b740f67..98b2d6d2e9 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -481,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 = in Array.equal eq_branch br1 br2 -(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *) +(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *) let rec hash_mllambda gn n env t = match t with | MLlocal ln -> combinesmall 1 (LNmap.find ln env) @@ -979,7 +979,7 @@ let compile_prim decl cond paux = let args = Array.map opt_prim_aux args in app_prim (Coq_primitive(op,None)) args (* - TODO: check if this inling was useful + TODO: check if this inlining was useful begin match op with | Int31lt -> if Sys.word_size = 64 then |