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.

1 files changed, 10 insertions, 2 deletions

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)