diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-19 07:05:18 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-19 07:05:18 +0200 |
| commit | c85e668255c1a2ef7881a7a106bffebd8f171f28 (patch) | |
| tree | a5b04be90577a2da3cc26f3c35f9aa66b17cfa7e /interp/constrintern.ml | |
| parent | fa141fa1d2df2720f84a3e2c1fc4900a47f9939f (diff) | |
Fix anomaly on user-inputted projection name (bug #5029).
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c4688f9f..30016dedc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1078,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1094,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) |