Slight improvement in naming existential variables.

In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.

1 files changed, 22 insertions, 9 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index ff13676818..f0ee8ae68f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1174,12 +1174,34 @@ let meta_declare mv v ?(name=Anonymous) evd =
   let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
   set_metas evd metas
 
+(* If the meta is defined then forget its name *)
+let meta_name evd mv =
+  try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+
+let evar_source_of_meta mv evd =
+  match meta_name evd mv with
+  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
+
+let use_meta_source evd mv v =
+  match Constr.kind v with
+  | Evar (evk,_) ->
+    let f = function
+    | None -> None
+    | Some evi as x ->
+      match evi.evar_source with
+      | None, Evar_kinds.GoalEvar -> Some { evi with evar_source = evar_source_of_meta mv evd }
+      | _ -> x in
+    { evd with undf_evars = EvMap.update evk f evd.undf_evars }
+  | _ -> evd
+
 let meta_assign mv (v, pb) evd =
   let modify _ = function
   | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
   | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.")
   in
   let metas = Metamap.modify mv modify evd.metas in
+  let evd = use_meta_source evd mv v in
   set_metas evd metas
 
 let meta_reassign mv (v, pb) evd =
@@ -1190,10 +1212,6 @@ let meta_reassign mv (v, pb) evd =
   let metas = Metamap.modify mv modify evd.metas in
   set_metas evd metas
 
-(* If the meta is defined then forget its name *)
-let meta_name evd mv =
-  try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
-
 let clear_metas evd = {evd with metas = Metamap.empty}
 
 let meta_merge ?(with_univs = true) evd1 evd2 =
@@ -1217,11 +1235,6 @@ let retract_coercible_metas evd =
   let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
-let evar_source_of_meta mv evd =
-  match meta_name evd mv with
-  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
-  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
-
 let dependent_evar_ident ev evd =
   let evi = find evd ev in
   match evi.evar_source with