From 7ae07d738b7b2704971b8bc2becb7a1355deb5c3 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Thu, 14 Jun 2018 00:09:54 +0200 Subject: [TYPO FIX] elimitate -> eliminate --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') 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 -- cgit v1.2.3