From 1300da19d13f7e46cf3a4b0b3396604ffc44a6d5 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jun 2018 22:03:25 +0200 Subject: Change QuestionMark for better record field missing error message. While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. --- pretyping/glob_ops.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'pretyping/glob_ops.ml') diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 4dfa789ba..9ed0090ed 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -562,7 +562,11 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> - GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Define false; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x -- cgit v1.2.3