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.
---
 engine/evar_kinds.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'engine/evar_kinds.ml')

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 12e2fda8e2..bedfd0cbbd 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -21,12 +21,21 @@ 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;
+}
+
 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
-- 
cgit v1.2.3


From 83afcfd21be0084b2eff33ffd9e2d8b785679d4a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat
Date: Tue, 17 Jul 2018 01:14:36 +0200
Subject: change into QuestionMark default

---
 engine/evar_kinds.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/evar_kinds.ml')

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index bedfd0cbbd..ea1e572548 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -30,6 +30,12 @@ type question_mark = {
      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 *)
-- 
cgit v1.2.3