Merge PR #7941: Extend QuestionMark to produce a better error message in case of missing record field

1 files changed, 16 insertions, 1 deletions

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 12e2fda8e..ea1e57254 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -21,12 +21,27 @@ type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
 
 type subevar_kind = Domain | Codomain | Body
 
+(* maybe this should be a Projection.t *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+     qm_obligation: obligation_definition_status;
+     qm_name: Name.t;
+     qm_record_field: record_field option;
+}
+
+let default_question_mark = {
+  qm_obligation=Define true;
+  qm_name=Anonymous;
+  qm_record_field=None;
+}
+
 type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
-  | QuestionMark of obligation_definition_status * Name.t
+  | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int