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/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index b4afb6415..12d31e5f4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -754,7 +754,7 @@ let mark_in_evm ~goal evd content = - GoalEvar (morally not dependent) - VarInstance (morally dependent of some name). This is a heuristic for naming these evars. *) - | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } -- cgit v1.2.3