diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 15:21:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 15:21:19 +0200 |
| commit | 31e13998542941040343cb81787a1d7c865d5b65 (patch) | |
| tree | c8fa54eaa323e189bf19f45f0dc42e1670908b1c | |
| parent | 1098604f599aa9aae9f07cf4960f41ef34f865e5 (diff) | |
| parent | 7ae07d738b7b2704971b8bc2becb7a1355deb5c3 (diff) | |
Merge PR #7803: [TYPO FIX] elimitate -> eliminate
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7345b701..47ae64d47 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1313,7 +1313,7 @@ let sort_fields ~complete loc fields completer = first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) = - (* elimitate the first field from the projections, + (* eliminate the first field from the projections, but keep its index *) let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc = match projs with |