aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml2
1 files changed, 1 insertions, 1 deletions
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 }