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.

4 files changed, 24 insertions, 5 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2d72b9db6..6a63fb02f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2104,7 +2104,10 @@ let mk_JMeq_refl evdref typ x =
   papp evdref coq_JMeq_refl [| typ; x |]
 
 let hole na = DAst.make @@
-  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
+  GHole (Evar_kinds.QuestionMark {
+      Evar_kinds.qm_obligation= Evar_kinds.Define false;
+      Evar_kinds.qm_name=na;
+      Evar_kinds.qm_record_field=None},
          IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5c4cbefad..7b4b2d42f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -98,7 +98,11 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
 open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
-  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
+  let src = Loc.tag ?loc (Evar_kinds.QuestionMark {
+      Evar_kinds.qm_obligation=Evar_kinds.Define opaque;
+      Evar_kinds.qm_name=na;
+      Evar_kinds.qm_record_field=None;
+  }) in
   let evd, v = Evarutil.new_evar env !evdref ~src c in
   evdref := evd;
   v
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
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57c4d363b..122979c1a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -381,8 +381,16 @@ let adjust_evar_source evdref na c =
   | Name id, Evar (evk,args) ->
      let evi = Evd.find !evdref evk in
      begin match evi.evar_source with
-     | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
-        let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+     | loc, Evar_kinds.QuestionMark {
+         Evar_kinds.qm_obligation=b;
+         Evar_kinds.qm_name=Anonymous;
+         Evar_kinds.qm_record_field=recfieldname;
+        } ->
+        let src = (loc,Evar_kinds.QuestionMark {
+            Evar_kinds.qm_obligation=b;
+            Evar_kinds.qm_name=na;
+            Evar_kinds.qm_record_field=recfieldname;
+        }) in
         let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in
         evdref := evd;
         mkEvar (evk',args)