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/termops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 2b179c43b..e4c8ae66b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -114,7 +114,7 @@ let pr_evar_suggested_name evk sigma = | None -> match evi.evar_source with | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id | _,Evar_kinds.VarInstance id -> id - | _,Evar_kinds.QuestionMark (_,Name id) -> id + | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in -- cgit v1.2.3